:: AFF_4 semantic presentation begin theorem :: AFF_4:1 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "a9"))) "or" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "a9")) "," (Set (Var "a"))) ")" ) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool "ex" (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) ")" )))) ; theorem :: AFF_4:2 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) ")" ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; theorem :: AFF_4:3 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "," (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) ")" ) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K"))) ")" )))) ; theorem :: AFF_4:4 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) ")" ) & (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) ")" )))) ; theorem :: AFF_4:5 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "M"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "M"))) ")" ) & (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "N"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "N"))) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N")))))) ; theorem :: AFF_4:6 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "M"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "M"))) ")" ) & (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_aff_1 :::"//"::: ) (Set (Var "M"))) "or" (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r2_aff_1 :::"//"::: ) (Set (Var "M"))) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: AFF_4:7 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) "or" (Bool (Set (Var "C")) ($#r5_aff_1 :::"//"::: ) (Set (Var "A"))) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))))) ; theorem :: AFF_4:8 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "a9"))) ")" ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "a9")))) "holds" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))))) ; theorem :: AFF_4:9 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "a9"))) ")" ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))))) ; theorem :: AFF_4:10 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) "or" (Bool (Set (Var "N")) ($#r5_aff_1 :::"//"::: ) (Set (Var "M"))) ")" ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "a9"))) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))))) ; theorem :: AFF_4:11 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" )))) ; theorem :: AFF_4:12 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool "not" (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "K", "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); func :::"Plane"::: "(" "K" "," "P" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "AS" equals :: AFF_4:def 1 "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" "AS" : (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "AS" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) "K") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "P") ")" )) "}" ; end; :: deftheorem defines :::"Plane"::: AFF_4:def 1 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) : (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) ")" )) "}" ))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); attr "X" is :::"being_plane"::: means :: AFF_4:def 2 (Bool "ex" (Set (Var "K")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AS" "st" (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Bool "not" (Set (Var "K")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P")))) & (Bool "X" ($#r1_hidden :::"="::: ) (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" )) ")" )); end; :: deftheorem defines :::"being_plane"::: AFF_4:def 2 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) "iff" (Bool "ex" (Set (Var "K")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Bool "not" (Set (Var "K")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P")))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" )) ")" )) ")" ))); theorem :: AFF_4:13 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Bool "not" (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ))) "holds" (Bool (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: AFF_4:14 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" )))) ; theorem :: AFF_4:15 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: AFF_4:16 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) ($#r5_aff_1 :::"//"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "M")) "," (Set (Var "P")) ")" )))) ; theorem :: AFF_4:17 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Bool "not" (Set (Var "P")) ($#r5_aff_1 :::"//"::: ) (Set (Var "Q"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) ")" ))))) ; theorem :: AFF_4:18 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Bool "not" (Set (Var "P")) ($#r5_aff_1 :::"//"::: ) (Set (Var "Q"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) ")" ))))) ; theorem :: AFF_4:19 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "X")))))) ; theorem :: AFF_4:20 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Bool "not" (Set (Var "K")) ($#r5_aff_1 :::"//"::: ) (Set (Var "Q")))) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" ))) "holds" (Bool (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" )))) ; theorem :: AFF_4:21 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set ($#k1_aff_4 :::"Plane"::: ) "(" (Set (Var "K")) "," (Set (Var "P")) ")" )) & (Bool (Bool "not" (Set (Var "P")) ($#r5_aff_1 :::"//"::: ) (Set (Var "Q"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) ")" )))) ; theorem :: AFF_4:22 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Bool "not" (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) ")" )))) ; theorem :: AFF_4:23 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool "(" (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) "or" (Bool (Set (Var "N")) ($#r5_aff_1 :::"//"::: ) (Set (Var "M"))) ")" )) "holds" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))))) ; theorem :: AFF_4:24 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v1_aff_1 :::"being_line"::: ) )))) ; theorem :: AFF_4:25 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))))) ; theorem :: AFF_4:26 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); let "K" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); assume (Bool (Set (Const "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ; func "a" :::"*"::: "K" -> ($#m1_subset_1 :::"Subset":::) "of" "AS" means :: AFF_4:def 3 (Bool "(" (Bool "a" ($#r2_hidden :::"in"::: ) it) & (Bool "K" ($#r5_aff_1 :::"//"::: ) it) ")" ); end; :: deftheorem defines :::"*"::: AFF_4:def 3 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "K")))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) & (Bool (Set (Var "K")) ($#r5_aff_1 :::"//"::: ) (Set (Var "b4"))) ")" ) ")" ))))); theorem :: AFF_4:27 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "A"))) "is" ($#v1_aff_1 :::"being_line"::: ) )))) ; theorem :: AFF_4:28 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))))) ; theorem :: AFF_4:29 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))))) ; theorem :: AFF_4:30 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )))) ; theorem :: AFF_4:31 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k2_aff_4 :::"*"::: ) (Set (Var "A")) ")" )))))) ; theorem :: AFF_4:32 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) ($#r5_aff_1 :::"//"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "M"))))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "X", "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); pred "X" :::"'||'"::: "Y" means :: AFF_4:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "AS" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AS" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "Y") & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) "X")) "holds" (Bool (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) "Y"))); end; :: deftheorem defines :::"'||'"::: AFF_4:def 4 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))))) ")" ))); theorem :: AFF_4:33 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool "(" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" ) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))))) ; theorem :: AFF_4:34 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) ")" )))) ; theorem :: AFF_4:35 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Bool "not" (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) ")" )))) ; theorem :: AFF_4:36 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" ))))) ; theorem :: AFF_4:37 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" )))) ; theorem :: AFF_4:38 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" ))))) ; theorem :: AFF_4:39 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" )))) ; theorem :: AFF_4:40 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) "iff" (Bool (Set (Var "M")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "N"))) ")" ))) ; theorem :: AFF_4:41 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool "(" (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) "or" (Bool (Set (Var "N")) ($#r5_aff_1 :::"//"::: ) (Set (Var "M"))) ")" ) ")" )) ")" ))) ; theorem :: AFF_4:42 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "M")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))))) ; theorem :: AFF_4:43 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "K", "M", "N" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); pred "K" "," "M" "," "N" :::"is_coplanar"::: means :: AFF_4:def 5 (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AS" "st" (Bool "(" (Bool "K" ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool "M" ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool "N" ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" )); end; :: deftheorem defines :::"is_coplanar"::: AFF_4:def 5 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) ($#r2_aff_4 :::"is_coplanar"::: ) ) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" )) ")" ))); theorem :: AFF_4:44 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) ($#r2_aff_4 :::"is_coplanar"::: ) )) "holds" (Bool "(" (Bool (Set (Var "K")) "," (Set (Var "N")) "," (Set (Var "M")) ($#r2_aff_4 :::"is_coplanar"::: ) ) & (Bool (Set (Var "M")) "," (Set (Var "K")) "," (Set (Var "N")) ($#r2_aff_4 :::"is_coplanar"::: ) ) & (Bool (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "K")) ($#r2_aff_4 :::"is_coplanar"::: ) ) & (Bool (Set (Var "N")) "," (Set (Var "K")) "," (Set (Var "M")) ($#r2_aff_4 :::"is_coplanar"::: ) ) & (Bool (Set (Var "N")) "," (Set (Var "M")) "," (Set (Var "K")) ($#r2_aff_4 :::"is_coplanar"::: ) ) ")" ))) ; theorem :: AFF_4:45 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "K")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "K")) ($#r2_aff_4 :::"is_coplanar"::: ) ) & (Bool (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "A")) ($#r2_aff_4 :::"is_coplanar"::: ) ) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "M")) "," (Set (Var "K")) "," (Set (Var "A")) ($#r2_aff_4 :::"is_coplanar"::: ) ))) ; theorem :: AFF_4:46 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "X")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "K")) ($#r1_hidden :::"<>"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "A")) ($#r2_aff_4 :::"is_coplanar"::: ) ) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))) ; theorem :: AFF_4:47 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "(" (Bool (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "M")) ($#r2_aff_4 :::"is_coplanar"::: ) ) & (Bool (Set (Var "M")) "," (Set (Var "K")) "," (Set (Var "M")) ($#r2_aff_4 :::"is_coplanar"::: ) ) & (Bool (Set (Var "M")) "," (Set (Var "M")) "," (Set (Var "K")) ($#r2_aff_4 :::"is_coplanar"::: ) ) ")" )))) ; theorem :: AFF_4:48 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "AS")) "is" (Bool "not" ($#l1_analoaf :::"AffinPlane":::))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool "not" (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))))) ; theorem :: AFF_4:49 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "AS")) "is" (Bool "not" ($#l1_analoaf :::"AffinPlane":::))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "P"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9")))))) ; theorem :: AFF_4:50 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set (Var "AS")) "is" (Bool "not" ($#l1_analoaf :::"AffinPlane":::)))) "holds" (Bool (Set (Var "AS")) "is" ($#v4_aff_2 :::"Desarguesian"::: ) )) ; theorem :: AFF_4:51 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "AS")) "is" (Bool "not" ($#l1_analoaf :::"AffinPlane":::))) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P"))) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "P"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9")))))) ; theorem :: AFF_4:52 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set (Var "AS")) "is" (Bool "not" ($#l1_analoaf :::"AffinPlane":::)))) "holds" (Bool (Set (Var "AS")) "is" ($#v11_aff_2 :::"translational"::: ) )) ; theorem :: AFF_4:53 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::)) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds" (Bool "ex" (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" )))) ; theorem :: AFF_4:54 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Set (Var "a9")) ($#r1_hidden :::"<>"::: ) (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9")))) "holds" (Bool "ex" (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" )))) ; theorem :: AFF_4:55 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool "(" (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "M"))) "or" (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "A"))) ")" ) & (Bool "(" (Bool (Set (Var "P")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) "or" (Bool (Set (Var "N")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P"))) ")" ) ")" )) ")" ))) ; theorem :: AFF_4:56 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "M")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))))) ; theorem :: AFF_4:57 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))))) ; theorem :: AFF_4:58 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))))) ; theorem :: AFF_4:59 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: AFF_4:60 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Z"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Z"))))) ; theorem :: AFF_4:61 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Z")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool "(" (Bool "(" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Z"))) ")" ) "or" (Bool "(" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Z")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" ) "or" (Bool "(" (Bool (Set (Var "Y")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Z"))) ")" ) "or" (Bool "(" (Bool (Set (Var "Y")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" ) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Z"))))) ; theorem :: AFF_4:62 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))))) ; theorem :: AFF_4:63 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Z")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z")))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z"))))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: AFF_4:64 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Z")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z")))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z")))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z"))) ($#r5_aff_1 :::"//"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z"))))))) ; theorem :: AFF_4:65 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" ))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); assume (Bool (Set (Const "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ; func "a" :::"+"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "AS" means :: AFF_4:def 6 (Bool "(" (Bool "a" ($#r2_hidden :::"in"::: ) it) & (Bool "X" ($#r1_aff_4 :::"'||'"::: ) it) & (Bool it "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" ); end; :: deftheorem defines :::"+"::: AFF_4:def 6 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_aff_4 :::"+"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "b4"))) & (Bool (Set (Var "b4")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" ) ")" ))))); theorem :: AFF_4:66 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Set (Var "a")) ($#k3_aff_4 :::"+"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" )))) ; theorem :: AFF_4:67 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k3_aff_4 :::"+"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_aff_4 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k3_aff_4 :::"+"::: ) (Set (Var "X")) ")" )))))) ; theorem :: AFF_4:68 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_aff_4 :::"*"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k3_aff_4 :::"+"::: ) (Set (Var "X"))))))) ; theorem :: AFF_4:69 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_aff_4 :::"+"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_aff_4 :::"+"::: ) (Set (Var "Y"))))))) ;