:: AFF_1 semantic presentation begin definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "a", "b", "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); pred :::"LIN"::: "a" "," "b" "," "c" means :: AFF_1:def 1 (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "a" "," "c"); end; :: deftheorem defines :::"LIN"::: AFF_1:def 1 : (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")) "holds" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" ))); theorem :: AFF_1:1 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))))) ; theorem :: AFF_1:2 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "x"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))) ; theorem :: AFF_1:3 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "z"))) & (Bool (Set (Var "z")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))) ; theorem :: AFF_1:4 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t")))) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "z"))) & (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "z"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "x"))) & (Bool (Set (Var "t")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "t")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "x"))) ")" ))) ; theorem :: AFF_1:5 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool "(" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) ")" ) ")" )) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))))) ; theorem :: AFF_1:6 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")))) "holds" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x"))) ")" ))) ; theorem :: AFF_1:7 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "x")) "," (Set (Var "y"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "y"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x"))) ")" ))) ; theorem :: AFF_1:8 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")))) "holds" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u"))))) ; theorem :: AFF_1:9 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t")))) "holds" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t"))))) ; theorem :: AFF_1:10 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))))) ; theorem :: AFF_1:11 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "z"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "u")) "," (Set (Var "z")) "," (Set (Var "w")))) "holds" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w"))))) ; theorem :: AFF_1:12 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")))))) ; theorem :: AFF_1:13 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))))))) ; theorem :: AFF_1:14 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b9")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); func :::"Line"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "AS" means :: AFF_1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "AS" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool ($#r1_aff_1 :::"LIN"::: ) "a" "," "b" "," (Set (Var "x"))) ")" )); end; :: deftheorem defines :::"Line"::: AFF_1:def 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 "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x"))) ")" )) ")" )))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); :: original: :::"Line"::: redefine func :::"Line"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "AS"; commutativity (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")) "holds" (Bool (Set ($#k1_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_aff_1 :::"Line"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ))) ; end; theorem :: AFF_1:15 (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")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ))) ; theorem :: AFF_1:16 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; theorem :: AFF_1:17 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (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 ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); attr "A" is :::"being_line"::: means :: AFF_1:def 3 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "AS" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )); end; :: deftheorem defines :::"being_line"::: AFF_1:def 3 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) ")" ))); registrationlet "AS" be ($#l1_analoaf :::"AffinSpace":::); cluster ($#v1_aff_1 :::"being_line"::: ) for bbbadM1_SUBSET_1((Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AS")))); end; theorem :: AFF_1:18 (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 "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C")))))) ; theorem :: AFF_1:19 (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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "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")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" )))) ; theorem :: AFF_1:20 (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 "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; theorem :: AFF_1:21 (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")) "holds" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (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 "A"))) ")" )) ")" ))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); pred "a" "," "b" :::"//"::: "A" means :: AFF_1:def 4 (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "AS" "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )); end; :: deftheorem defines :::"//"::: AFF_1:def 4 : (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")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" )))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "A", "C" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); pred "A" :::"//"::: "C" means :: AFF_1:def 5 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "AS" "st" (Bool "(" (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) "C") ")" )); end; :: deftheorem defines :::"//"::: AFF_1:def 5 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r3_aff_1 :::"//"::: ) (Set (Var "C"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "C"))) ")" )) ")" ))); theorem :: AFF_1:22 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ))) ; theorem :: AFF_1:23 (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 (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) ")" )))) ; theorem :: AFF_1: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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" ) ")" )))) ; theorem :: AFF_1:25 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "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"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; theorem :: AFF_1:26 (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 "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ))) ; theorem :: AFF_1:27 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "," (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 (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )))) ; theorem :: AFF_1:28 (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 (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ))))) ; theorem :: AFF_1:29 (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")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; theorem :: AFF_1:30 (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" ($#v1_aff_1 :::"being_line"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" )))) ; theorem :: AFF_1:31 (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" ($#v1_aff_1 :::"being_line"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: AFF_1:32 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (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")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A")))))) ; theorem :: AFF_1:33 (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" ($#v1_aff_1 :::"being_line"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A")))))) ; theorem :: AFF_1:34 (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 (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A")))))) ; theorem :: AFF_1:35 (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 (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool "not" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))) ; theorem :: AFF_1:36 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) ($#r3_aff_1 :::"//"::: ) (Set (Var "C")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" ))) ; theorem :: AFF_1:37 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r3_aff_1 :::"//"::: ) (Set (Var "C"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" )) ")" ))) ; theorem :: AFF_1:38 (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" ($#v1_aff_1 :::"being_line"::: ) ($#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 "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r3_aff_1 :::"//"::: ) (Set (Var "C"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )))) ; theorem :: AFF_1:39 (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 (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"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r3_aff_1 :::"//"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: AFF_1:40 (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 "C")) "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")) ($#r3_aff_1 :::"//"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "C")))))) ; theorem :: AFF_1:41 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "being" ($#v1_aff_1 :::"being_line"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool (Set (Var "A")) ($#r3_aff_1 :::"//"::: ) (Set (Var "A"))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "A", "B" be ($#v1_aff_1 :::"being_line"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); :: original: :::"//"::: redefine pred "A" :::"//"::: "B"; reflexivity (Bool "for" (Set (Var "A")) "being" ($#v1_aff_1 :::"being_line"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")) "holds" (Bool ((Set (Const "AS")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: AFF_1:42 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) ($#r3_aff_1 :::"//"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "C")) ($#r3_aff_1 :::"//"::: ) (Set (Var "A"))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "A", "C" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); :: original: :::"//"::: redefine pred "A" :::"//"::: "C"; symmetry (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")) "st" (Bool (Bool ((Set (Const "AS")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "AS")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: AFF_1:43 (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 "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "C")))))) ; theorem :: AFF_1:44 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r5_aff_1 :::"//"::: ) (Set (Var "D"))) ")" ) "or" (Bool "(" (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) & (Bool (Set (Var "D")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) ")" ) "or" (Bool "(" (Bool (Set (Var "C")) ($#r5_aff_1 :::"//"::: ) (Set (Var "A"))) & (Bool (Set (Var "C")) ($#r5_aff_1 :::"//"::: ) (Set (Var "D"))) ")" ) "or" (Bool "(" (Bool (Set (Var "C")) ($#r5_aff_1 :::"//"::: ) (Set (Var "A"))) & (Bool (Set (Var "D")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "D"))))) ; theorem :: AFF_1:45 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "p")) "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 (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C")))))) ; theorem :: AFF_1:46 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) "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 "x")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool "not" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b"))))))) ; theorem :: AFF_1:47 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "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 "a9")) "," (Set (Var "b9")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))))) ; theorem :: AFF_1:48 (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" ($#v1_aff_1 :::"being_line"::: ) ($#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 "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; theorem :: AFF_1:49 (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" ($#v1_aff_1 :::"being_line"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) ")" ))))) ; theorem :: AFF_1:50 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "D"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "D")))))) ; theorem :: AFF_1:51 (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 (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (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 "A"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: AFF_1:52 (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 (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A")))))) ; theorem :: AFF_1:53 (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 "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C")))))) ; theorem :: AFF_1:54 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (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 "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))) "holds" (Bool "(" (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "o"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "o"))) ")" ))) ; theorem :: AFF_1:55 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "o")))) "holds" (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "o"))))) ; theorem :: AFF_1:56 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "x")))) "holds" (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: AFF_1:57 (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 (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; theorem :: AFF_1:58 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Bool "not" (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )))) ; theorem :: AFF_1:59 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x"))) ")" ))))) ; theorem :: AFF_1:60 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP")) "st" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p"))) ")" )))) ;