:: PROJRED2 semantic presentation begin definitionlet "IPS" be ($#l1_incsp_1 :::"IncProjSp":::); let "A", "B", "C" be ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "IPS")); pred "A" "," "B" "," "C" :::"are_concurrent"::: means :: PROJRED2:def 1 (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" "IPS") "st" (Bool "(" (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) "A") & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) "B") & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) "C") ")" )); end; :: deftheorem defines :::"are_concurrent"::: PROJRED2:def 1 : (Bool "for" (Set (Var "IPS")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPS")) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) ) "iff" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set (Var "IPS"))) "st" (Bool "(" (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))) ")" )) ")" ))); definitionlet "IPS" be ($#l1_incsp_1 :::"IncProjSp":::); let "Z" be ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "IPS")); func :::"CHAIN"::: "Z" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" "IPS") equals :: PROJRED2:def 2 "{" (Set (Var "z")) where z "is" ($#m1_subset_1 :::"POINT":::) "of" "IPS" : (Bool (Set (Var "z")) ($#r1_incsp_1 :::"on"::: ) "Z") "}" ; end; :: deftheorem defines :::"CHAIN"::: PROJRED2:def 2 : (Bool "for" (Set (Var "IPS")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPS")) "holds" (Bool (Set ($#k1_projred2 :::"CHAIN"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "z")) where z "is" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPS")) : (Bool (Set (Var "z")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Z"))) "}" ))); definitionlet "IPP" be ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::); mode :::"Projection"::: "of" "IPP" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" "IPP") "," (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" "IPP") means :: PROJRED2:def 3 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IPP"(Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IPP" "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "B")) ")" )) ")" ))); end; :: deftheorem defines :::"Projection"::: PROJRED2:def 3 : (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set (Var "IPP"))) "," (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set (Var "IPP"))) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_projred2 :::"Projection"::: ) "of" (Set (Var "IPP"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP"))(Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "B")) ")" )) ")" ))) ")" ))); theorem :: PROJRED2:1 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) "or" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) ))) ; theorem :: PROJRED2:2 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "A")) ($#r1_projred2 :::"are_concurrent"::: ) ) ")" ))) ; theorem :: PROJRED2:3 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Set (Var "y")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "o")) "," (Set (Var "B")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))))) ; theorem :: PROJRED2:4 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "o")) "," (Set (Var "B")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_projred2 :::"CHAIN"::: ) (Set (Var "A"))))))) ; theorem :: PROJRED2:5 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "o")) "," (Set (Var "B")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_projred2 :::"CHAIN"::: ) (Set (Var "B"))))))) ; theorem :: PROJRED2:6 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_projred2 :::"CHAIN"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) ")" )) ")" )))) ; theorem :: PROJRED2:7 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "o")) "," (Set (Var "B")) ")" ) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; theorem :: PROJRED2:8 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "o")) "," (Set (Var "B")) ")" ")" ) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "B")) "," (Set (Var "o")) "," (Set (Var "A")) ")" ))))) ; theorem :: PROJRED2:9 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "f")) "being" ($#m1_projred2 :::"Projection"::: ) "of" (Set (Var "IPP")) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ) "is" ($#m1_projred2 :::"Projection"::: ) "of" (Set (Var "IPP"))))) ; theorem :: PROJRED2:10 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "o")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_projred2 :::"CHAIN"::: ) (Set (Var "A")) ")" )))))) ; theorem :: PROJRED2:11 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_projred2 :::"CHAIN"::: ) (Set (Var "A")) ")" )) "is" ($#m1_projred2 :::"Projection"::: ) "of" (Set (Var "IPP"))))) ; theorem :: PROJRED2:12 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "C")) "," (Set (Var "o")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "o")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "o")) "," (Set (Var "B")) ")" ))))) ; theorem :: PROJRED2:13 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "o1")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O1")))) & (Bool (Bool "not" (Set (Var "o1")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O2")))) & (Bool (Bool "not" (Set (Var "o2")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O2")))) & (Bool (Bool "not" (Set (Var "o2")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O3")))) & (Bool (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O3")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Set (Var "O1")) ($#r1_hidden :::"<>"::: ) (Set (Var "O3")))) "holds" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O1")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O3")))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "O2")) "," (Set (Var "o2")) "," (Set (Var "O3")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "O1")) "," (Set (Var "o1")) "," (Set (Var "O2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "O1")) "," (Set (Var "o")) "," (Set (Var "O3")) ")" )) ")" ))))) ; theorem :: PROJRED2:14 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "pp9")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "Q")) "," (Set (Var "O")) "," (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Bool "not" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "O")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O1"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O1"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O1"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O2"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O2"))) & (Bool (Set (Var "pp9")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O2"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O3"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O3"))) & (Bool (Set (Var "pp9")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O3"))) & (Bool (Set (Var "pp9")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))))) "holds" (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "C")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "Q")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "q")) "," (Set (Var "Q")) ")" ")" )))))) ; theorem :: PROJRED2:15 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "o")) "," (Set (Var "o99")) "," (Set (Var "d")) "," (Set (Var "o9")) "," (Set (Var "oo9")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "Q")) "," (Set (Var "O")) "," (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "o")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "o99")) "," (Set (Var "d")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "oo9")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "o9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "o9")) "," (Set (Var "oo9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "oo9")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O3"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O")))) "holds" (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "C")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "Q")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "q")) "," (Set (Var "Q")) ")" ")" )))))) ; theorem :: PROJRED2:16 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "d")) "," (Set (Var "q")) "," (Set (Var "pp9")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "Q")) "," (Set (Var "B")) "," (Set (Var "O")) "," (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Bool "not" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "O")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "p")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "pp9")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "p")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "pp9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "pp9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O3")))) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) ")" )))) ; theorem :: PROJRED2:17 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o")) "," (Set (Var "o99")) "," (Set (Var "d")) "," (Set (Var "o9")) "," (Set (Var "oo9")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "Q")) "," (Set (Var "O")) "," (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "o")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "o99")) "," (Set (Var "d")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "oo9")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "o9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "o9")) "," (Set (Var "oo9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "oo9")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O3"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) ")" )))) ; theorem :: PROJRED2:18 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "d")) "," (Set (Var "pp9")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "O")) "," (Set (Var "Q")) "," (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Bool "not" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "O")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "p")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "pp9")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "p")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "pp9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "pp9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O3")))) "holds" (Bool "(" (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set (Var "A"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) ")" )))) ; theorem :: PROJRED2:19 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "o")) "," (Set (Var "o99")) "," (Set (Var "d")) "," (Set (Var "o9")) "," (Set (Var "oo9")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "O")) "," (Set (Var "Q")) "," (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "o")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "o99")) "," (Set (Var "d")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "oo9")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "o9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "o9")) "," (Set (Var "oo9")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "oo9")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O3"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q"))) ")" )))) ; theorem :: PROJRED2:20 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "Q")) "," (Set (Var "O")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "Q")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "C")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "Q")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "q")) "," (Set (Var "Q")) ")" ")" ))) ")" ))))) ; theorem :: PROJRED2:21 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "Q")) "," (Set (Var "O")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) )) & (Bool (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "Q")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "C")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "Q")) "," (Set (Var "q")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "Q")) ")" ")" ))) ")" ))))) ; theorem :: PROJRED2:22 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "s")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "S")) "," (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R"))) & (Bool (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R"))) & (Bool (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "C")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "Q")) "," (Set (Var "a")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "b")) "," (Set (Var "Q")) ")" ")" )))))) ; theorem :: PROJRED2:23 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "O")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) ))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "Q")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "C")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "Q")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "q")) "," (Set (Var "Q")) ")" ")" ))) ")" ))))) ; theorem :: PROJRED2:24 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "O")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "O"))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_projred2 :::"are_concurrent"::: ) ))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "Q")) ($#r1_projred2 :::"are_concurrent"::: ) ) & (Bool (Bool "not" (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "C")) "," (Set (Var "b")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "Q")) "," (Set (Var "q")) "," (Set (Var "B")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "Q")) ")" ")" ))) ")" ))))) ;