:: DIRAF semantic presentation begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"lambda"::: "R" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) ) means :: DIRAF:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") "or" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "c")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" )); end; :: deftheorem defines :::"lambda"::: DIRAF:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_diraf :::"lambda"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "or" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "c")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" )) ")" ))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; func :::"Lambda"::: "S" -> ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffinStruct"::: ) equals :: DIRAF:def 2 (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "(" ($#k1_diraf :::"lambda"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "S") ")" ) "#)" ); end; :: deftheorem defines :::"Lambda"::: DIRAF:def 2 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "(" ($#k1_diraf :::"lambda"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "S"))) ")" ) "#)" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; cluster (Set ($#k2_diraf :::"Lambda"::: ) "S") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ; end; theorem :: DIRAF:1 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: DIRAF:2 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t")))) "holds" (Bool "(" (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 "t")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "x"))) ")" ))) ; theorem :: DIRAF:3 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))))) ; theorem :: DIRAF:4 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) & (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "x"))) ")" ))) ; theorem :: DIRAF:5 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "z"))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "t"))))) ; theorem :: DIRAF:6 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))) "iff" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) "or" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "y"))) ")" ) ")" ))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; let "a", "b", "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); pred :::"Mid"::: "a" "," "b" "," "c" means :: DIRAF:def 3 (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "b" "," "c"); end; :: deftheorem defines :::"Mid"::: DIRAF:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" ))); theorem :: DIRAF:7 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))) "iff" (Bool "(" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) "or" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y"))) ")" ) ")" ))) ; theorem :: DIRAF:8 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: DIRAF:9 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) "holds" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))))) ; theorem :: DIRAF:10 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "x")) "," (Set (Var "y"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "y"))) ")" ))) ; theorem :: DIRAF:11 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: DIRAF:12 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: DIRAF:13 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "z"))) ")" )))) ; theorem :: DIRAF:14 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: DIRAF:15 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Bool "not" ($#r1_diraf :::"Mid"::: ) (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t"))))) "holds" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "y")) "," (Set (Var "t")) "," (Set (Var "z"))))) ; theorem :: DIRAF:16 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Bool "not" ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "t"))))) "holds" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "t")) "," (Set (Var "z"))))) ; theorem :: DIRAF:17 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Bool "not" ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))))) "holds" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y"))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); pred "a" "," "b" :::"'||'"::: "c" "," "d" means :: DIRAF:def 4 (Bool "(" (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "c" "," "d") "or" (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "d" "," "c") ")" ); end; :: deftheorem defines :::"'||'"::: DIRAF:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" ) ")" ))); theorem :: DIRAF:18 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_diraf :::"lambda"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "S"))))) ")" ))) ; theorem :: DIRAF:19 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "y")) "," (Set (Var "x"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))) ; theorem :: DIRAF:20 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "z"))) & (Bool (Set (Var "z")) "," (Set (Var "z")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))) ; theorem :: DIRAF:21 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "z")))) "holds" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_diraf :::"'||'"::: ) (Set (Var "y")) "," (Set (Var "z"))))) ; theorem :: DIRAF:22 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t")))) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "t")) "," (Set (Var "z"))) & (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_diraf :::"'||'"::: ) (Set (Var "t")) "," (Set (Var "z"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_diraf :::"'||'"::: ) (Set (Var "y")) "," (Set (Var "x"))) & (Bool (Set (Var "t")) "," (Set (Var "z")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "t")) "," (Set (Var "z")) ($#r2_diraf :::"'||'"::: ) (Set (Var "y")) "," (Set (Var "x"))) ")" ))) ; theorem :: DIRAF:23 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (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 "S")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool "(" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_diraf :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_diraf :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t"))) ")" ) ")" )) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t"))))) ; theorem :: DIRAF:24 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) "holds" (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "z")))))) ; theorem :: DIRAF:25 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_diraf :::"'||'"::: ) (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) ")" )))) ; theorem :: DIRAF:26 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_diraf :::"'||'"::: ) (Set (Var "y")) "," (Set (Var "t"))) ")" )))) ; theorem :: DIRAF:27 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "t")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "z")) "," (Set (Var "x")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_diraf :::"'||'"::: ) (Set (Var "t")) "," (Set (Var "u"))) ")" )))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; let "a", "b", "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); pred :::"LIN"::: "a" "," "b" "," "c" means :: DIRAF:def 5 (Bool "a" "," "b" ($#r2_diraf :::"'||'"::: ) "a" "," "c"); end; :: deftheorem defines :::"LIN"::: DIRAF:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool ($#r3_diraf :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" ))); notationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; let "a", "b", "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); synonym "a" "," "b" "," "c" :::"is_collinear"::: for :::"LIN"::: "a" "," "b" "," "c"; end; theorem :: DIRAF:28 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r3_diraf :::"is_collinear"::: ) ))) ; theorem :: DIRAF:29 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r3_diraf :::"is_collinear"::: ) ) "or" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "or" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))) "or" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))) ")" ))) ; theorem :: DIRAF:30 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#r3_diraf :::"is_collinear"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) ($#r3_diraf :::"is_collinear"::: ) ) ")" ))) ; theorem :: DIRAF:31 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "x")) "," (Set (Var "y")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "y")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x")) ($#r3_diraf :::"is_collinear"::: ) ) ")" ))) ; theorem :: DIRAF:32 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (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 "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ($#r3_diraf :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u")) ($#r3_diraf :::"is_collinear"::: ) ))) ; theorem :: DIRAF:33 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t")) ($#r3_diraf :::"is_collinear"::: ) ))) ; theorem :: DIRAF:34 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t")) ($#r3_diraf :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t"))))) ; theorem :: DIRAF:35 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (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 "S")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "z"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#r3_diraf :::"is_collinear"::: ) ) & (Bool (Set (Var "u")) "," (Set (Var "z")) "," (Set (Var "w")) ($#r3_diraf :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) ($#r3_diraf :::"is_collinear"::: ) ))) ; theorem :: DIRAF:36 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) "holds" (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#r3_diraf :::"is_collinear"::: ) )))) ; theorem :: DIRAF:37 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "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 "S")) "st" (Bool (Bool "not" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#r3_diraf :::"is_collinear"::: ) ))))) ; theorem :: DIRAF:38 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "st" (Bool (Bool (Set (Var "AS")) ($#r1_hidden :::"="::: ) (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "S"))))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "c9"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "d9")))) "holds" (Bool "(" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ))))) ; theorem :: DIRAF:39 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "st" (Bool (Bool (Set (Var "AS")) ($#r1_hidden :::"="::: ) (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "S"))))) "holds" (Bool "(" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "w")) "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 "z")) "," (Set (Var "z"))) & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))) ")" & "(" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z")))) "implies" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) ")" ")" ) ")" ) & (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (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"))) & (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) ")" )) ")" ) & (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 "z")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "u"))) ")" )) ")" ) ")" ))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"AffinSpace-like"::: means :: DIRAF:def 6 (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "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 "z")) "," (Set (Var "z"))) & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))) ")" & "(" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z")))) "implies" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) ")" ")" ) ")" ) & (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "z")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "u"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"AffinSpace-like"::: DIRAF:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_diraf :::"AffinSpace-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "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 "z")) "," (Set (Var "z"))) & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))) ")" & "(" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z")))) "implies" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) ")" ")" ) ")" ) & (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "z")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "u"))) ")" )) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v1_diraf :::"AffinSpace-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode AffinSpace is ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_diraf :::"AffinSpace-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: DIRAF:40 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool "(" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "w")) "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 "z")) "," (Set (Var "z"))) & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))) ")" & "(" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z")))) "implies" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) ")" ")" ) ")" ) & (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (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"))) & (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) ")" )) ")" ) & (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 "z")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "u"))) ")" )) ")" ) ")" )) ; theorem :: DIRAF:41 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinSpace":::) "holds" (Bool (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "S"))) "is" ($#l1_analoaf :::"AffinSpace":::))) ; theorem :: DIRAF:42 (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool "(" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "w")) "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 "z")) "," (Set (Var "z"))) & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))) ")" & "(" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z")))) "implies" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) ")" ")" ) ")" ) & (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (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"))) & (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) ")" )) ")" ) & (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 "z")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "u"))) ")" )) ")" ) ")" ) "iff" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinSpace":::)) ")" )) ; theorem :: DIRAF:43 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinPlane":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "t"))))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_diraf :::"'||'"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_diraf :::"'||'"::: ) (Set (Var "z")) "," (Set (Var "u"))) ")" )))) ; theorem :: DIRAF:44 (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinPlane":::) "st" (Bool (Bool (Set (Var "AS")) ($#r1_hidden :::"="::: ) (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "S"))))) "holds" (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 (Bool "not" (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "u"))) ")" ))))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"2-dimensional"::: means :: DIRAF:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Bool "not" (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "u"))) ")" ))); end; :: deftheorem defines :::"2-dimensional"::: DIRAF:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_diraf :::"2-dimensional"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "u"))) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v1_diraf :::"AffinSpace-like"::: ) ($#v2_diraf :::"2-dimensional"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode AffinPlane is ($#v2_diraf :::"2-dimensional"::: ) ($#l1_analoaf :::"AffinSpace":::); end; theorem :: DIRAF:45 (Bool "for" (Set (Var "S")) "being" ($#l1_analoaf :::"OAffinPlane":::) "holds" (Bool (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "S"))) "is" ($#l1_analoaf :::"AffinPlane":::))) ; theorem :: DIRAF:46 (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::)) "iff" (Bool "(" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "w")) "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 "z")) "," (Set (Var "z"))) & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))) ")" & "(" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z")))) "implies" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) ")" ")" ) ")" ) & (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (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"))) & (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "t"))) ")" )) ")" ) & (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 "z")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "t"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "y")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "u"))) ")" )) ")" ) & (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 (Bool "not" (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "u"))) & (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "u"))) ")" )) ")" ) ")" ) ")" )) ;