(def-constant connecting%lines"lambda(s:sets[points], indic{ll:sets[points], line(ll) and 2<=f_card{s inters ll}})"(theory geometry-3))

(def-theorem cardinality-at-least-2-lemma"forall(s:sets[ind_1], 2<=f_card{s} implies forsome(a,b:ind_1, a in s and b in s and not(a=b)))"lemma (theory generic-theory-1) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(n:nn, f_card{s}=n)") (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(n:nn,2<=n);") (antecedent-inference"with(p:prop,p);") (backchain"with(p:prop,p);") (incorporate-antecedent"with(p:prop,p);") (apply-macete-with-minor-premises iota-free-definition-of-f-card) direct-and-antecedent-inference-strategy (contrapose"with(f:sets[nn],f=f);") (unfold-single-defined-constant (0) omega) (contrapose"with(p:prop,forall(a,b:ind_1,p and p implies a=b));") (cut-with-single-formula"forsome(a,b:ind_1, a in s and b in s and f(a)=0 and f(b)=1)") (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(a,b:ind_1,p));") (instantiate-existential ("a""b")) (antecedent-inference"with(p:prop,p and p and p and p);") (contrapose"with(n:nn,n=1);") simplify (backchain-backwards"with(b,a:ind_1,a=b);") simplify ) (block (script-comment"`cut-with-single-formula' at (1)") (incorporate-antecedent"with(f:sets[nn],f=f);") (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f:[nn,prop],pred_to_indic(f)) subseteq with(f:[ind_1,nn],ran{f});") (move-to-ancestor 1) (instantiate-universal-antecedent-multiply"with(f:[nn,prop],pred_to_indic(f)) subseteq with(f:[ind_1,nn],ran{f});"(("0") ("1")) ) (block (script-comment"`instantiate-universal-antecedent-multiply' at (0 0 0 0 0)") (contrapose"with(f:sets[nn],not(1 in f));") simplify-insistently ) (block (script-comment"`instantiate-universal-antecedent-multiply' at (0 0 0 0 1)") (contrapose"with(p:prop,not(p));") simplify-insistently ) (block (script-comment"`instantiate-universal-antecedent-multiply' at (0 0 0 1 0)") (contrapose"with(p:prop,not(p));") simplify-insistently ) (block (script-comment"`instantiate-universal-antecedent-multiply' at (0 0 0 1 1)") (incorporate-antecedent"with(f:sets[nn],1 in f);") (incorporate-antecedent"with(f:sets[nn],0 in f);") simplify-insistently direct-and-antecedent-inference-strategy (instantiate-existential ("x_$0""x_$1")) (block (script-comment"`instantiate-existential' at (0 0 0 (1 . 0))") (backchain-backwards"with(s,f:sets[ind_1],f=s);") simplify-insistently (apply-macete-with-minor-premises tr%domain-membership-iff-defined) ) (block (script-comment"`instantiate-existential' at (0 1)") (backchain-backwards"with(s,f:sets[ind_1],f=s);") (apply-macete-with-minor-premises tr%domain-membership-iff-defined) ) ) ) ) (instantiate-existential ("f_card{s}")) )))

(def-theorem cardinality-at-most-1-lemma"forall(s:sets[ind_1], f_card{s}<=1 implies (empty_indic_q{s} or forsome(a:ind_1, s=singleton{a})))"lemma (theory generic-theory-1) (usages transportable-macete) (proof ( direct-inference direct-inference (cut-with-single-formula"f_card{s}=0 or f_card{s}=1") (move-to-sibling 1) simplify (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,p or p);") (block (script-comment"`antecedent-inference' at (0)") (incorporate-antecedent"with(n:nn,n=0);") (apply-macete-with-minor-premises empty-indic-has-f-card-zero) direct-inference (backchain"with(f,s:sets[ind_1],s=f);") (weaken (0 1)) simplify-insistently) (block (script-comment"`antecedent-inference' at (1)") (incorporate-antecedent"with(n:nn,n=1);") (apply-macete-with-minor-premises singleton-has-f-card-one) simplify)) )))

(def-theorem cardinality-at-least-2"forall(s:sets[ind_1], f_indic_q{s} implies (2<=f_card{s} iff forsome(a,b:ind_1, a in s and b in s and not(a=b))))"(theory generic-theory-1) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises cardinality-at-least-2-lemma) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)") (cut-with-single-formula"not (empty_indic_q{s} or forsome(a:ind_1, s=singleton{a}))") (block (script-comment"`cut-with-single-formula' at (0)") (contrapose"with(p:prop,not(p or p));") (apply-macete-with-minor-premises cardinality-at-most-1-lemma) simplify) (block (script-comment"`cut-with-single-formula' at (1)") (contrapose"with(p:prop,not(p));") (antecedent-inference"with(p:prop,p or p);") (instantiate-universal-antecedent"with(s:sets[ind_1],empty_indic_q{s});"("a")) (block (script-comment"`antecedent-inference' at (1)") (antecedent-inference"with(p:prop,forsome(a:ind_1,p));") (contrapose"with(f,s:sets[ind_1],s=f);") (apply-macete-with-minor-premises tr%subseteq-antisymmetry) (contrapose"with(p:prop,not(p));") (antecedent-inference"with(p:prop,p and p);") (contrapose"with(a_$0:ind_1,s:sets[ind_1],s subseteq singleton{a_$0});") (apply-macete-with-minor-premises tr%in-singleton-iff-equals-single-member) (case-split ("a=a_$0")) (block (script-comment"`case-split' at (1)") (instantiate-existential ("b")) simplify) (instantiate-existential ("a"))))) )))

(def-theorem cardinality-at-least-3-lemma"forall(s:sets[ind_1], 3<=f_card{s} implies forsome(a,b,c:ind_1, a in s and b in s and c in s and not(a=b) and not(a=c) and not(b=c)))"lemma (theory generic-theory-1) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(n:nn, f_card{s}=n)") (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(n:nn,3<=n);") (antecedent-inference"with(p:prop,p);") (backchain"with(p:prop,p);") (incorporate-antecedent"with(p:prop,p);") (apply-macete-with-minor-premises iota-free-definition-of-f-card) direct-and-antecedent-inference-strategy (contrapose"with(f:sets[nn],f=f);") (unfold-single-defined-constant (0) omega) (contrapose"with(p:prop,forall(a,b,c:ind_1,p));") (cut-with-single-formula"forsome(a,b,c:ind_1, a in s and b in s and c in s and f(a)=0 and f(b)=1 and f(c)=2)") (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(a,b,c:ind_1,p));") (instantiate-existential ("a""b""c")) (block (script-comment"`instantiate-existential' at (0 3)") (contrapose"with(p:prop,p and p and p and p and p and p);") simplify) (block (script-comment"`instantiate-existential' at (0 4)") (contrapose"with(p:prop,p and p and p and p and p and p);") simplify) (block (script-comment"`instantiate-existential' at (0 5)") (contrapose"with(p:prop,p and p and p and p and p and p);") simplify)) (block (script-comment"`cut-with-single-formula' at (1)") (incorporate-antecedent"with(f:sets[nn],f=f);") (apply-macete-with-minor-premises tr%indic-free-characterization-of-ran) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-universal-antecedent-multiply"with(p:prop,forall(y_$0:nn,p));"(("0") ("1") ("2"))) (block (script-comment"`instantiate-universal-antecedent-multiply' at (0 0 0 0 0 0 0 0 0 0)") (instantiate-existential ("x_$1""x_$2""x_$0")) (block (script-comment"`instantiate-existential' at (0 0 0 (1 . 0))") (backchain-backwards"with(s,f:sets[ind_1],f=s);") simplify (apply-macete-with-minor-premises tr%domain-membership-iff-defined)) (block (script-comment"`instantiate-existential' at (0 1)") (backchain-backwards"with(s,f:sets[ind_1],f=s);") (apply-macete-with-minor-premises tr%domain-membership-iff-defined)) (block (script-comment"`instantiate-existential' at (0 2)") (backchain-backwards"with(s,f:sets[ind_1],f=s);") (apply-macete-with-minor-premises tr%domain-membership-iff-defined))) (simplify-antecedent"with(p:prop,not(p));") (simplify-antecedent"with(p:prop,not(p));") (simplify-antecedent"with(n:nn,not(2<n));") (simplify-antecedent"with(p:prop,not(p));") (block (script-comment"`instantiate-universal-antecedent-multiply' at (0 0 0 0 1 0 0 1)") (simplify-antecedent"with(n:nn,not(0<n));") (simplify-antecedent"with(p:prop,not(p));")) (block (script-comment"`instantiate-universal-antecedent-multiply' at (0 0 0 0 1 1 0 0)") (simplify-antecedent"with(n:nn,not(0<n));") (simplify-antecedent"with(p:prop,not(p));")) (simplify-antecedent"with(n:nn,not(1<n));"))) (instantiate-existential ("f_card{s}")))))

(def-theorem injectivity-of-trace"forall(s:sets[points], injective_on_q{lambda(ll:sets[points], if(ll in connecting%lines(s), s inters ll, ?sets[points])), connecting%lines(s)})"(theory geometry-3) (proof ( direct-inference insistent-direct-inference beta-reduce-repeatedly (unfold-single-defined-constant-globally connecting%lines) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (cut-with-single-formula" forsome(a,b:points, a in s inters x_1 and b in s inters x_1 and not(a=b))") (block (script-comment"`cut-with-single-formula' at (0)") (simplify-antecedent"with(f:sets[points],f=f);") (antecedent-inference"with(p:prop,forsome(a,b:points,p));") (apply-macete-with-minor-premises two-points-determine-a-line) (instantiate-existential ("b""a")) (block (script-comment"`instantiate-existential' at (0 3)") (antecedent-inference"with(p:prop,p and p and p);") (incorporate-antecedent"with(a:points,x_1,s:sets[points],a in s inters x_1);") simplify-insistently) (block (script-comment"`instantiate-existential' at (0 4)") (antecedent-inference"with(p:prop,p and p and p);") (incorporate-antecedent"with(b:points,x_1,s:sets[points],b in s inters x_1);") simplify-insistently) (block (script-comment"`instantiate-existential' at (0 5)") (incorporate-antecedent"with(p:prop,p and p and p);") (backchain-repeatedly ("with(x_2,x_1,s:sets[points],s inters x_1=s inters x_2);")) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(a:points,x_2,s:sets[points],a in s inters x_2);") simplify-insistently) (block (script-comment"`instantiate-existential' at (0 6)") (incorporate-antecedent"with(p:prop,p and p and p);") (backchain-repeatedly ("with(x_2,x_1,s:sets[points],s inters x_1=s inters x_2);")) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(b:points,x_2,s:sets[points],b in s inters x_2);") simplify-insistently)) (apply-macete-with-minor-premises tr%cardinality-at-least-2-lemma) )))

(def-translation generic-theory-1-to-geometry (source generic-theory-1) (target geometry-3) (fixed-theories h-o-real-arithmetic) (sort-pairs (ind_1 points)) (theory-interpretation-check using-simplification))

(def-transported-symbols power (translation generic-theory-1-to-geometry))

(def-theorem cardinality-of-connecting%lines-bound"forall(s:sets[points], f_indic_q{s} implies f_card{connecting%lines(s)}<=f_card{power(s)})"(theory geometry-3) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%f-card-leq-iff-finite-and-embeds) (block (script-comment"`apply-macete-with-minor-premises' at (0)") direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0)") (cut-with-single-formula"f_card{power(s)}=2^f_card{s}") (apply-macete-with-minor-premises tr%power-card) simplify) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1)") (instantiate-existential ("lambda(ll:sets[points], if(ll in connecting%lines(s), s inters ll,?sets[points]))")) (block (script-comment"`instantiate-existential' at (0 0)") (apply-macete-with-minor-premises tr%subseteq-antisymmetry) (block (script-comment"`apply-macete-with-minor-premises' at (0)") direct-and-antecedent-inference-strategy simplify-insistently simplify-insistently) (unfold-single-defined-constant (0) connecting%lines)) (block (script-comment"`instantiate-existential' at (0 1)") (unfold-single-defined-constant (0) power) insistent-direct-inference (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly simplify direct-and-antecedent-inference-strategy (backchain"with(f,x_$11:sets[points],x_$11=f);") simplify-insistently (weaken (0)) simplify-insistently) (apply-macete-with-minor-premises injectivity-of-trace))) (unfold-single-defined-constant (0) power) (unfold-single-defined-constant (0) connecting%lines) )))

(def-theorem connecting%lines-of-finite-sets-are-finite"forall(s:sets[points], f_indic_q{s} implies f_indic_q{connecting%lines(s)})"(theory geometry-3) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forall(s:sets[points], f_indic_q{s} implies f_card{connecting%lines(s)}<=f_card{power(s)})") (block (script-comment"`cut-with-single-formula' at (0)") (apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (instantiate-universal-antecedent"with(p:prop,forall(s:sets[points],p));"("s")) (instantiate-existential ("f_card{connecting%lines(s)}"))) (unfold-single-defined-constant (0) connecting%lines)) (apply-macete-with-minor-premises cardinality-of-connecting%lines-bound) )))

(def-constant on%connecting%line"lambda(s:sets[points], indic{x:points, forsome(l:sets[points], l in connecting%lines(s) and x in l)})"(theory geometry-3))

(def-theorem lines-exist"forsome(l:sets[points], line(l))"(theory geometry-2) (proof ( (cut-with-single-formula"forsome(a,b:points, not a =b)") (move-to-sibling 1) (apply-macete-with-minor-premises at-least-two-points) (block (script-comment"`cut-with-single-formula' at (0)") (instantiate-existential ("le(a,b)")) (apply-macete-with-minor-premises le-is-a-line)) )))

(def-atomic-sort lines"line"(theory geometry-2))

(def-constant trace%on%line"lambda(l:lines, lambda(m:lines, iota(x:points, x in l and x in m)))"(theory geometry-3))

(def-theorem iota-free-characterization-of-trace%on%line"forall(l,m:lines, x:points, not l=m implies (trace%on%line(l)(m)=x iff (x in l and x in m)))"(theory geometry-3) (proof ( (unfold-single-defined-constant (0) trace%on%line) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0)") (contrapose"with(x,p:points,p=x);") (apply-macete-with-minor-premises eliminate-iota-macete) (contrapose"with(x:points,l:lines,not(x in l));")) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 1)") (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy (contrapose"with(x,p:points,p=x);") (apply-macete-with-minor-premises eliminate-iota-macete) (contrapose"with(x:points,m:lines,not(x in m));")) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1 0)") (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises two-points-determine-a-line) auto-instantiate-existential simplify (apply-macete-with-minor-premises lines-in-quasi-sort_geometry-2) (apply-macete-with-minor-premises lines-in-quasi-sort_geometry-2)) )))

(def-theorem trace%on%line-undefined-case"forall(l,m:lines, x:points, l=m implies not #(trace%on%line(l)(m)))"(theory geometry-3) (proof ( direct-and-antecedent-inference-strategy (unfold-single-defined-constant-globally trace%on%line) (apply-macete-with-minor-premises eliminate-iota-macete) (contrapose"with(p:prop,p);") (antecedent-inference"with(p:prop,p);") (antecedent-inference"with(p:prop,p);") (contrapose"with(p:prop,forall(j:points,p));") simplify (cut-with-single-formula"forsome(a,b:points, a in l and b in l and not(a=b))") (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(a,b:points,p));") (case-split ("a=i")) (block (script-comment"`case-split' at (1)") (instantiate-existential ("b")) simplify) (instantiate-existential ("a"))) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises lines-contain-two-points) (apply-macete-with-minor-premises lines-in-quasi-sort_geometry-2)) )))

(def-theorem on%connecting%line-characterization"forall(s:sets[points], l:lines, not l in connecting%lines(s) implies image{trace%on%line(l), connecting%lines(s)}= on%connecting%line(s) inters l)"reverse (theory geometry-3) (proof ( (apply-macete-with-minor-premises tr%subseteq-antisymmetry) simplify-insistently direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0 0 0)") (backchain"with(p,x_$2:points,x_$2=p);") (unfold-single-defined-constant (0) on%connecting%line) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly auto-instantiate-existential (cut-with-single-formula"trace%on%line(l)(x)=x_$2") (incorporate-antecedent"with(x_$2:points,x:sets[points],f:[lines,points],f(x)=x_$2);") (apply-macete-with-minor-premises iota-free-characterization-of-trace%on%line) simplify (block (script-comment"`apply-macete-with-minor-premises' at (1)") (contrapose"with(p:prop,not(p));") simplify)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 1 0 0)") (cut-with-single-formula"trace%on%line(l)(x)=x_$2") (incorporate-antecedent"with(x_$2:points,x:sets[points],f:[lines,points],f(x)=x_$2);") (apply-macete-with-minor-premises iota-free-characterization-of-trace%on%line) simplify (block (script-comment"`apply-macete-with-minor-premises' at (1)") (contrapose"with(p:prop,not(p));") simplify)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1 0 0 0)") (force-substitution" x_$1=trace%on%line(l)(x)""trace%on%line(l)(x)=x_$1"(0)) (move-to-sibling 1) simplify (block (script-comment"`force-substitution' at (0)") (apply-macete-with-minor-premises iota-free-characterization-of-trace%on%line) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (incorporate-antecedent"with(x_$1:points,s:sets[points], x_$1 in on%connecting%line(s));") (unfold-single-defined-constant (0) on%connecting%line) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (instantiate-existential ("l_$0"))) (block (script-comment"`apply-macete-with-minor-premises' at (1)") (contrapose"with(p:prop,not(p));") simplify) (block (script-comment"`apply-macete-with-minor-premises' at (2)") (apply-macete-with-minor-premises lines-defining-axiom_geometry-2) (incorporate-antecedent"with(x:sets[points],f:sets[sets[points]],x in f);") (unfold-single-defined-constant (0) connecting%lines) (apply-macete-with-minor-premises indicator-facts-macete) simplify))) )))

(def-theorem finitely-many-on%connecting%line"forall(s:sets[points], l:lines, f_indic_q{s} and not l in connecting%lines(s) implies f_indic_q(on%connecting%line(s) inters l))"(theory geometry-3) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"f_card{on%connecting%line(s) inters l}<=f_card{connecting%lines(s)}") (apply-macete-with-minor-premises rev%on%connecting%line-characterization) (apply-macete-with-minor-premises tr%image-of-a-finite-set-is-finite) (apply-macete-with-minor-premises connecting%lines-of-finite-sets-are-finite) (unfold-single-defined-constant (0) trace%on%line) (unfold-single-defined-constant (0) connecting%lines) )))

(def-constant connecting%lines%through"lambda(s:sets[points], p:points, indic{l:sets[points], p in l and l in connecting%lines(s)})"(theory geometry-3))

(def-constant on%connecting%line%through"lambda(s:sets[points], p:points, indic{x:points, forsome(l:sets[points], x in l and l in connecting%lines%through(s,p))})"(theory geometry-3))

(def-theorem on%connecting%line%through-characterization"forall(s:sets[points], p:points, l:lines, not p in l implies image{trace%on%line(l), connecting%lines%through(s,p)}= on%connecting%line%through(s,p) inters l)"reverse (theory geometry-3) (proof ( (apply-macete-with-minor-premises tr%subseteq-antisymmetry) simplify-insistently direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0 0 0 0)") (backchain"with(p,x_$2:points,x_$2=p);") (unfold-single-defined-constant (0) on%connecting%line%through) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly (instantiate-existential ("x")) (cut-with-single-formula"trace%on%line(l)(x)=x_$2") (backchain"with(x_$2:points,x:sets[points],f:[lines,points],f(x)=x_$2);") (incorporate-antecedent"with(x_$2:points,x:sets[points],f:[lines,points],f(x)=x_$2);") (apply-macete-with-minor-premises iota-free-characterization-of-trace%on%line) simplify (block (script-comment"`apply-macete-with-minor-premises' at (1)") (contrapose"with(p,x_$2:points,x_$2=p);") (cut-with-single-formula"not #(trace%on%line(l)(x))") (contrapose"with(p:points,not(#(p)));") (apply-macete-with-minor-premises trace%on%line-undefined-case))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0 1 0 0)") (cut-with-single-formula"trace%on%line(l)(x)=x_$2") (incorporate-antecedent"with(x_$2:points,x:sets[points],f:[lines,points],f(x)=x_$2);") (apply-macete-with-minor-premises iota-free-characterization-of-trace%on%line) simplify (block (script-comment"`apply-macete-with-minor-premises' at (1)") (contrapose"with(p,x_$2:points,x_$2=p);") (cut-with-single-formula"not #(trace%on%line(l)(x))") (contrapose"with(p:points,not(#(p)));") (apply-macete-with-minor-premises trace%on%line-undefined-case))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1 0 0 0 0)") (instantiate-existential ("x_$1")) (incorporate-antecedent"with(x_$1,p:points,s:sets[points], x_$1 in on%connecting%line%through(s,p));") (unfold-single-defined-constant (0) on%connecting%line%through) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (instantiate-existential ("l_$0")) (force-substitution"x_$1=trace%on%line(l)(l_$0)""x_$1=trace%on%line(l)(l_$0)"(0)) (force-substitution"x_$1=trace%on%line(l)(l_$0)""trace%on%line(l)(l_$0)=x_$1"(0)) (move-to-sibling 1) simplify (block (script-comment"`force-substitution' at (0)") (apply-macete-with-minor-premises iota-free-characterization-of-trace%on%line) direct-and-antecedent-inference-strategy (block (script-comment"`apply-macete-with-minor-premises' at (1)") (contrapose"with(p:prop,not(p));") (backchain"with(l_$0:sets[points],l:lines,l=l_$0);") (incorporate-antecedent"with(l_$0:sets[points],f:sets[sets[points]],l_$0 in f);") (unfold-single-defined-constant (0) connecting%lines%through) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly simplify) (block (script-comment"`apply-macete-with-minor-premises' at (2)") (apply-macete-with-minor-premises lines-defining-axiom_geometry-2) (incorporate-antecedent"with(l_$0:sets[points],f:sets[sets[points]],l_$0 in f);") (unfold-single-defined-constant (0) connecting%lines%through) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly (unfold-single-defined-constant (0) connecting%lines) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly simplify))) )))

(def-theorem finitely-many-on%connecting%line%through"forall(s:sets[points], l:lines, p:points, f_indic_q{s} and not p in l implies f_indic_q(on%connecting%line%through(s,p) inters l))"(theory geometry-3) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"f_card{on%connecting%line%through(s,p) inters l}<= f_card{connecting%lines%through(s,p)}") (apply-macete-with-minor-premises rev%on%connecting%line%through-characterization) (apply-macete-with-minor-premises tr%image-of-a-finite-set-is-finite) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (instantiate-existential ("connecting%lines(s)")) (block (script-comment"`instantiate-existential' at (0 0)") (unfold-single-defined-constant (0) connecting%lines%through) simplify-insistently) (apply-macete-with-minor-premises connecting%lines-of-finite-sets-are-finite) (unfold-single-defined-constant (0) connecting%lines)) (unfold-single-defined-constant (0) connecting%lines%through)) (unfold-single-defined-constant (0) trace%on%line) )))

(def-theorem lines-are-infinite"forall(l:lines,s:sets[points], f_indic_q{s} implies forsome(x:points, x in l and not x in s))"(theory geometry-4) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(a,b:points, a in l and b in l and not(a=b))") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises lines-contain-two-points) (apply-macete-with-minor-premises lines-in-quasi-sort_geometry-2)) (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(a,b:points,p));") (case-split (" nonempty_indic_q{s inters l diff singleton{a} }")) (block (script-comment"`case-split' at (1)") (cut-with-single-formula"forsome(x:points, x in (s inters l diff singleton{a}) and forall(y:points, y in (s inters l diff singleton{a}) implies not(bet(a,y,x)))) ") (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference-strategy (0)) (cut-with-single-formula"forsome(z:points, bet(a,z,x))") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises existence-middle) (incorporate-antecedent"with(x:points,f:sets[points],x in f);") simplify-insistently) (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(x,a:points,forsome(z:points,bet(a,z,x)));") (instantiate-existential ("z")) (block (script-comment"`instantiate-existential' at (0 0)") (cut-with-single-formula"line(l)") (cut-with-single-formula"l=le(a,b)") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises lines-are-le) simplify) (block (script-comment"`cut-with-single-formula' at (0)") (cut-with-single-formula"coll%closed(l)") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (backchain"with(f:sets[points],l:lines,l=f);") (apply-macete-with-minor-premises le-is-coll%closed)) (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(l:lines,coll%closed(l));") (unfold-single-defined-constant (0) coll%closed) direct-and-antecedent-inference-strategy (backchain"with(p:prop,forall(a,b,x:points,p));") (instantiate-existential ("a""x")) (block (script-comment"`instantiate-existential' at (0 1)") (incorporate-antecedent"with(x:points,f:sets[points],x in f diff f);") simplify-insistently) (block (script-comment"`instantiate-existential' at (0 2)") (apply-macete-with-minor-premises collinear-all-cases) direct-and-antecedent-inference-strategy)))) (block (script-comment"`instantiate-existential' at (0 1)") (instantiate-universal-antecedent"with(p:prop,forall(y:points,p));"("z")) (contrapose"with(p:prop,not(p));") simplify-insistently (force-substitution"z=a""a=z"(0)) (move-to-sibling 1) simplify (block (script-comment"`force-substitution' at (0)") (apply-macete-with-minor-premises distinctness-1-2) auto-instantiate-existential)))) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises empty-segment-lemma) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite) (instantiate-existential ("s")) simplify-insistently)) (block (script-comment"`case-split' at (2)") (contrapose"with(p:prop,not(p));") simplify-insistently (instantiate-existential ("b")) simplify simplify)) ) ) )

(def-theorem le-contains-left-point"forall(x,y:points, #(le(x,y)) implies x in le(x,y))"(theory geometry-1) (proof ( (unfold-single-defined-constant-globally le) simplify )))

(def-compound-macete le-contains-point (series le-contains-left-point le-is-symmetric le-contains-left-point))

(def-theorem les-are-connecting-lines"forall(s:sets[points], x,y:points, f_indic_q{s} and x in s and y in s and not(x=y) implies le(x,y) in connecting%lines(s))"(theory geometry-4) (proof ( direct-and-antecedent-inference-strategy (unfold-single-defined-constant-globally connecting%lines) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises le-is-a-line) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1)") (apply-macete-with-minor-premises tr%cardinality-at-least-2) (block (script-comment"`apply-macete-with-minor-premises' at (0)") simplify-insistently auto-instantiate-existential (block (script-comment"`auto-instantiate-existential' at (0 1)") (apply-macete-with-minor-premises le-contains-point) (apply-macete-with-minor-premises le-is-symmetric)) (apply-macete-with-minor-premises le-contains-point)) (block (script-comment"`apply-macete-with-minor-premises' at (1)") (apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite) (instantiate-existential ("s")) simplify-insistently)) )))