:: PROJRED1 semantic presentation begin theorem :: PROJRED1:1 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "holds" (Bool "not" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "holds" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))))))) ; theorem :: PROJRED1:2 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "holds" (Bool "not" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "holds" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))))))) ; theorem :: PROJRED1:3 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (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 "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) ")" )))) ; theorem :: PROJRED1:4 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (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 "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) ")" )))) ; theorem :: PROJRED1:5 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set (Var "A"))) ")" )))) ; theorem :: PROJRED1:6 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "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")))) ")" )))) ; theorem :: PROJRED1:7 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))))) ; theorem :: PROJRED1:8 (Bool "for" (Set (Var "IPP")) "being" ($#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")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" ))))) ; theorem :: PROJRED1:9 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "ex" (Set (Var "A")) "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 "A")))) ")" )))) ; theorem :: PROJRED1:10 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "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 "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q")))))) ; theorem :: PROJRED1:11 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) ")" )))) ; theorem :: PROJRED1:12 (Bool "for" (Set (Var "IPP")) "being" ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "a2")) "," (Set (Var "b3")) "," (Set (Var "a3")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "," (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "a2")) "," (Set (Var "b2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "a3")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "a2")) "," (Set (Var "t")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "r")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "s")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "t")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "r")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "s")) "," (Set (Var "b2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O"))))))) ; theorem :: PROJRED1:13 (Bool "for" (Set (Var "IPP")) "being" ($#l1_incsp_1 :::"IncProjSp":::) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP"))(Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) ")" )))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) ")" )))) ; theorem :: PROJRED1:14 (Bool "for" (Set (Var "IPP")) "being" ($#v8_incproj :::"Fanoian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP"))(Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "Q")) "," (Set (Var "L")) "," (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Bool "not" (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S")))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "L"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "R"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "r")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))) ")" )))) ; theorem :: PROJRED1:15 (Bool "for" (Set (Var "IPP")) "being" ($#v8_incproj :::"Fanoian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP"))(Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) ")" )))) ; theorem :: PROJRED1:16 (Bool "for" (Set (Var "IPP")) "being" ($#v8_incproj :::"Fanoian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP"))(Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) ")" )))) ; theorem :: PROJRED1:17 (Bool "for" (Set (Var "IPP")) "being" ($#v8_incproj :::"Fanoian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) ")" )))) ; definitionlet "IPP" be ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::); let "K", "L" be ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "IPP")); let "p" be ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "IPP")); assume that (Bool (Bool "not" (Set (Const "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Const "K")))) and (Bool (Bool "not" (Set (Const "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Const "L")))) ; func :::"IncProj"::: "(" "K" "," "p" "," "L" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" "IPP") "," (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" "IPP") means :: PROJRED1:def 1 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" "IPP")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IPP" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it)) "iff" (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) "K") ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IPP" "st" (Bool (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) "K") & (Bool (Set (Var "y")) ($#r1_incsp_1 :::"on"::: ) "L")) "holds" (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IPP" "st" (Bool "(" (Bool "p" ($#r1_incsp_1 :::"on"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "X"))) ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"IncProj"::: PROJRED1:def 1 : (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L"))))) "holds" (Bool "for" (Set (Var "b5")) "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 "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set (Var "IPP")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5")))) "iff" (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) & (Bool (Set (Var "y")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) "holds" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "X"))) ")" )) ")" ) ")" ) ")" ) ")" ))))); theorem :: PROJRED1:18 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) "holds" (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))) ; theorem :: PROJRED1:19 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) "holds" (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")))))) ; theorem :: PROJRED1:20 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "y")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))))) ; theorem :: PROJRED1:21 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" )))) "holds" (Bool (Set (Var "y")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))))) ; theorem :: PROJRED1:22 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "R")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R"))))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "L")) "," (Set (Var "q")) "," (Set (Var "R")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "L")) "," (Set (Var "q")) "," (Set (Var "R")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "L")) "," (Set (Var "q")) "," (Set (Var "R")) ")" ")" ))) ")" )))) ; theorem :: PROJRED1:23 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Set (Var "a1")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) & (Bool (Set (Var "b1")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "b1"))))))) ; theorem :: PROJRED1:24 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) & (Bool (Set (Var "x")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) "holds" (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: PROJRED1:25 (Bool "for" (Set (Var "IPP")) "being" ($#v5_incproj :::"2-dimensional"::: ) ($#v9_incproj :::"Desarguesian"::: ) ($#l1_incsp_1 :::"IncProjSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IPP")) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "R")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IPP")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R"))) & (Bool (Set (Var "K")) ($#r1_hidden :::"<>"::: ) (Set (Var "R")))) "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 "K")))) & (Bool (Bool "not" (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Set (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "L")) "," (Set (Var "q")) "," (Set (Var "R")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "p")) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_projred1 :::"IncProj"::: ) "(" (Set (Var "K")) "," (Set (Var "o")) "," (Set (Var "R")) ")" )) ")" ))))) ;