:: SEMI_AF1 semantic presentation begin definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"Semi_Affine_Space-like"::: means :: SEMI_AF1:def 1 (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" ) & (Bool "not" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "q"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "o")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "p"))) & (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Bool (Set (Var "o")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "b")))) "implies" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "d"))) & (Bool (Set (Var "p")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" )) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "c")))) & (Bool (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "a9"))) & (Bool (Set (Var "o")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "b9"))) & (Bool (Set (Var "o")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "a9")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "a9")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "a9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a1")) "," (Set (Var "a2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "a3"))) & (Bool (Set (Var "b1")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "b3"))) & (Bool (Set (Var "a1")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a2")) "," (Set (Var "b3")) ($#r2_analoaf :::"//"::: ) (Set (Var "a3")) "," (Set (Var "b2")))) "holds" (Bool (Set (Var "a3")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b3"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d")))) "holds" (Bool "not" (Bool (Set (Var "a")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) ")" ) ")" ); end; :: deftheorem defines :::"Semi_Affine_Space-like"::: SEMI_AF1:def 1 : (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_semi_af1 :::"Semi_Affine_Space-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" ) & (Bool "not" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "q"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "o")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "p"))) & (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Bool (Set (Var "o")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "b")))) "implies" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "d"))) & (Bool (Set (Var "p")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" )) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "c")))) & (Bool (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "a9"))) & (Bool (Set (Var "o")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "b9"))) & (Bool (Set (Var "o")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "a9")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "a9")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "a9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a1")) "," (Set (Var "a2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "a3"))) & (Bool (Set (Var "b1")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "b3"))) & (Bool (Set (Var "a1")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a2")) "," (Set (Var "b3")) ($#r2_analoaf :::"//"::: ) (Set (Var "a3")) "," (Set (Var "b2")))) "holds" (Bool (Set (Var "a3")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b3"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d")))) "holds" (Bool "not" (Bool (Set (Var "a")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_semi_af1 :::"Semi_Affine_Space-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode Semi_Affine_Space is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_semi_af1 :::"Semi_Affine_Space-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: SEMI_AF1:1 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: SEMI_AF1:2 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: SEMI_AF1:3 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))))) ; theorem :: SEMI_AF1:4 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:5 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))))) ; theorem :: SEMI_AF1:6 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) ")" ))) ; theorem :: SEMI_AF1:7 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" ))) ; theorem :: SEMI_AF1:8 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))))) ; theorem :: SEMI_AF1:9 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "d"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" ))) ; theorem :: SEMI_AF1:10 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) ")" ))) ; theorem :: SEMI_AF1:11 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "x"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "x")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))))) ; theorem :: SEMI_AF1:12 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "a"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "b")))) "holds" (Bool "not" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c")))))) ; theorem :: SEMI_AF1:13 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r"))))))) ; theorem :: SEMI_AF1:14 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b")))) ")" ))) ; theorem :: SEMI_AF1:15 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set (Var "s")))) "holds" (Bool "not" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))))) ; theorem :: SEMI_AF1:16 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "q")) "," (Set (Var "r"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "not" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r")))))) ; theorem :: SEMI_AF1:17 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "r"))))) ; theorem :: SEMI_AF1:18 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r1")))) & (Bool (Set (Var "p")) "," (Set (Var "r1")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r2"))) & (Bool (Set (Var "q")) "," (Set (Var "r1")) ($#r2_analoaf :::"//"::: ) (Set (Var "q")) "," (Set (Var "r2")))) "holds" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set (Var "r2"))))) ; theorem :: SEMI_AF1:19 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r1"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r2"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "q")) "," (Set (Var "r1"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "q")) "," (Set (Var "r2")))) "holds" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set (Var "r2"))))) ; theorem :: SEMI_AF1:20 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "or" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) "or" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:21 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))))) ; definitionlet "SAS" be ($#l1_analoaf :::"Semi_Affine_Space":::); let "a", "b", "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SAS")); pred "a" "," "b" "," "c" :::"is_collinear"::: means :: SEMI_AF1:def 2 (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "a" "," "c"); end; :: deftheorem defines :::"is_collinear"::: SEMI_AF1:def 2 : (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" ))); theorem :: SEMI_AF1:22 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a1")) "," (Set (Var "a3")) "," (Set (Var "a2")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a3")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a1")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a3")) "," (Set (Var "a1")) "," (Set (Var "a2")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a3")) "," (Set (Var "a2")) "," (Set (Var "a1")) ($#r1_semi_af1 :::"is_collinear"::: ) ) ")" ))) ; theorem :: SEMI_AF1:23 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "r"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "r")))) "holds" (Bool "not" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_semi_af1 :::"is_collinear"::: ) )))) ; theorem :: SEMI_AF1:24 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) "or" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ))) ; theorem :: SEMI_AF1:25 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_semi_af1 :::"is_collinear"::: ) ))))) ; theorem :: SEMI_AF1:26 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:27 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "not" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) )))) ; theorem :: SEMI_AF1:28 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "holds" (Bool "not" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ($#r1_semi_af1 :::"is_collinear"::: ) )))) ; theorem :: SEMI_AF1:29 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "x")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "x")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: SEMI_AF1:30 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (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 "SAS")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))))) ; theorem :: SEMI_AF1:31 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p1")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p2")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p1")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p2")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))))) ; theorem :: SEMI_AF1:32 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:33 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:34 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "d1")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "d2")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d2")))) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2"))))) ; theorem :: SEMI_AF1:35 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) ))) ; definitionlet "SAS" be ($#l1_analoaf :::"Semi_Affine_Space":::); let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SAS")); pred :::"parallelogram"::: "a" "," "b" "," "c" "," "d" means :: SEMI_AF1:def 3 (Bool "(" (Bool (Bool "not" "a" "," "b" "," "c" ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "c" "," "d") & (Bool "a" "," "c" ($#r2_analoaf :::"//"::: ) "b" "," "d") ")" ); end; :: deftheorem defines :::"parallelogram"::: SEMI_AF1:def 3 : (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ))); theorem :: SEMI_AF1:36 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) ")" ))) ; theorem :: SEMI_AF1:37 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) )) ")" ))) ; theorem :: SEMI_AF1:38 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a1")) "," (Set (Var "a3")) "," (Set (Var "a2")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a4")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a1")) "," (Set (Var "a4")) "," (Set (Var "a2")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a1")) "," (Set (Var "a3")) "," (Set (Var "a4")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a1")) "," (Set (Var "a4")) "," (Set (Var "a3")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a3")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a1")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a4")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a2")) "," (Set (Var "a4")) "," (Set (Var "a1")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a2")) "," (Set (Var "a4")) "," (Set (Var "a3")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a3")) "," (Set (Var "a1")) "," (Set (Var "a2")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a3")) "," (Set (Var "a2")) "," (Set (Var "a1")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a3")) "," (Set (Var "a1")) "," (Set (Var "a4")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a1")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a3")) "," (Set (Var "a2")) "," (Set (Var "a4")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a2")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a4")) "," (Set (Var "a1")) "," (Set (Var "a2")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a4")) "," (Set (Var "a2")) "," (Set (Var "a1")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a4")) "," (Set (Var "a1")) "," (Set (Var "a3")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a4")) "," (Set (Var "a3")) "," (Set (Var "a1")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a4")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "a4")) "," (Set (Var "a3")) "," (Set (Var "a2")) ($#r1_semi_af1 :::"is_collinear"::: ) )) ")" ))) ; theorem :: SEMI_AF1:39 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" "not" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))) "or" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ($#r1_semi_af1 :::"is_collinear"::: ) ) "or" "not" (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ($#r1_semi_af1 :::"is_collinear"::: ) ) ")" ))) ; theorem :: SEMI_AF1:40 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:41 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: SEMI_AF1:42 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))))) ; theorem :: SEMI_AF1:43 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "(" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c"))) ")" ))) ; theorem :: SEMI_AF1:44 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: SEMI_AF1:45 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d1"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d2")))) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2"))))) ; theorem :: SEMI_AF1:46 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "not" (Bool (Set (Var "a")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))))) ; theorem :: SEMI_AF1:47 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "not" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c")))))) ; theorem :: SEMI_AF1:48 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" )))) ; theorem :: SEMI_AF1:49 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "c")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))))) ; theorem :: SEMI_AF1:50 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "c")) "," (Set (Var "c9")))) "holds" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9"))))) ; theorem :: SEMI_AF1:51 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "c")) "," (Set (Var "c9")))) "holds" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9"))))) ; theorem :: SEMI_AF1:52 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "d")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "c")) "," (Set (Var "c9"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "d")) "," (Set (Var "d9")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))))) ; theorem :: SEMI_AF1:53 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "d")))) "holds" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))))) ; definitionlet "SAS" be ($#l1_analoaf :::"Semi_Affine_Space":::); let "a", "b", "r", "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SAS")); pred :::"congr"::: "a" "," "b" "," "r" "," "s" means :: SEMI_AF1:def 4 (Bool "(" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) "b") & (Bool "r" ($#r1_hidden :::"="::: ) "s") ")" ) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "SAS" "st" (Bool "(" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "p")) "," (Set (Var "q")) "," "a" "," "b") & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "p")) "," (Set (Var "q")) "," "r" "," "s") ")" )) ")" ); end; :: deftheorem defines :::"congr"::: SEMI_AF1:def 4 : (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool "(" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s"))) ")" )) ")" ) ")" ))); theorem :: SEMI_AF1:54 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: SEMI_AF1:55 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: SEMI_AF1:56 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b")) "," (Set (Var "a")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: SEMI_AF1:57 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:58 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:59 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ))) "holds" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:60 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:61 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool ($#r2_semi_af1 :::"parallelogram"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:62 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: SEMI_AF1:63 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: SEMI_AF1:64 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: SEMI_AF1:65 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:66 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: SEMI_AF1:67 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))))) ; theorem :: SEMI_AF1:68 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))))) ; theorem :: SEMI_AF1:69 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "(" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))) ")" ))) ; theorem :: SEMI_AF1:70 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q")) "," (Set (Var "s")))) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "s"))))) ; theorem :: SEMI_AF1:71 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "q"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "r")))) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "q"))))) ; theorem :: SEMI_AF1:72 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "o")) "," (Set (Var "p"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "o")) "," (Set (Var "o")) "," (Set (Var "q")))) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "p"))))) ; theorem :: SEMI_AF1:73 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "q"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "r")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "q")) "," (Set (Var "r"))))) ; theorem :: SEMI_AF1:74 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "o")) "," (Set (Var "p"))) & (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "b")) "," (Set (Var "o")) "," (Set (Var "o")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))))) ; definitionlet "SAS" be ($#l1_analoaf :::"Semi_Affine_Space":::); let "a", "b", "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SAS")); func :::"sum"::: "(" "a" "," "b" "," "o" ")" -> ($#m1_subset_1 :::"Element":::) "of" "SAS" means :: SEMI_AF1:def 5 (Bool ($#r3_semi_af1 :::"congr"::: ) "o" "," "a" "," "b" "," it); end; :: deftheorem defines :::"sum"::: SEMI_AF1:def 5 : (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) ")" )) "iff" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b5"))) ")" ))); definitionlet "SAS" be ($#l1_analoaf :::"Semi_Affine_Space":::); let "a", "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SAS")); func :::"opposite"::: "(" "a" "," "o" ")" -> ($#m1_subset_1 :::"Element":::) "of" "SAS" means :: SEMI_AF1:def 6 (Bool (Set ($#k1_semi_af1 :::"sum"::: ) "(" "a" "," it "," "o" ")" ) ($#r1_hidden :::"="::: ) "o"); end; :: deftheorem defines :::"opposite"::: SEMI_AF1:def 6 : (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_semi_af1 :::"opposite"::: ) "(" (Set (Var "a")) "," (Set (Var "o")) ")" )) "iff" (Bool (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "b4")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "o"))) ")" ))); definitionlet "SAS" be ($#l1_analoaf :::"Semi_Affine_Space":::); let "a", "b", "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SAS")); func :::"diff"::: "(" "a" "," "b" "," "o" ")" -> ($#m1_subset_1 :::"Element":::) "of" "SAS" equals :: SEMI_AF1:def 7 (Set ($#k1_semi_af1 :::"sum"::: ) "(" "a" "," (Set "(" ($#k2_semi_af1 :::"opposite"::: ) "(" "b" "," "o" ")" ")" ) "," "o" ")" ); end; :: deftheorem defines :::"diff"::: SEMI_AF1:def 7 : (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set ($#k3_semi_af1 :::"diff"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k2_semi_af1 :::"opposite"::: ) "(" (Set (Var "b")) "," (Set (Var "o")) ")" ")" ) "," (Set (Var "o")) ")" )))); theorem :: SEMI_AF1:75 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: SEMI_AF1:76 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "o")))))) ; theorem :: SEMI_AF1:77 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set "(" ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) ")" ")" ) "," (Set (Var "c")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o")) ")" ")" ) "," (Set (Var "o")) ")" )))) ; theorem :: SEMI_AF1:78 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "o")) ")" )))) ; theorem :: SEMI_AF1:79 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "o")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "o"))))) ; theorem :: SEMI_AF1:80 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "o")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "a")) "," (Set (Var "y")) "," (Set (Var "o")) ")" ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: SEMI_AF1:81 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool ($#r3_semi_af1 :::"congr"::: ) (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "o")) "," (Set ($#k2_semi_af1 :::"opposite"::: ) "(" (Set (Var "a")) "," (Set (Var "o")) ")" )))) ; theorem :: SEMI_AF1:82 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set ($#k2_semi_af1 :::"opposite"::: ) "(" (Set (Var "a")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_semi_af1 :::"opposite"::: ) "(" (Set (Var "b")) "," (Set (Var "o")) ")" ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: SEMI_AF1:83 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set ($#k2_semi_af1 :::"opposite"::: ) "(" (Set (Var "a")) "," (Set (Var "o")) ")" ) "," (Set ($#k2_semi_af1 :::"opposite"::: ) "(" (Set (Var "b")) "," (Set (Var "o")) ")" )))) ; theorem :: SEMI_AF1:84 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set ($#k2_semi_af1 :::"opposite"::: ) "(" (Set (Var "o")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "o"))))) ; theorem :: SEMI_AF1:85 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "o")) ")" ) "," (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "o")) ")" )))) ; theorem :: SEMI_AF1:86 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "o")) ")" ) "," (Set ($#k1_semi_af1 :::"sum"::: ) "(" (Set (Var "q")) "," (Set (Var "s")) "," (Set (Var "o")) ")" )))) ; theorem :: SEMI_AF1:87 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool (Set ($#k3_semi_af1 :::"diff"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "o"))) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: SEMI_AF1:88 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool (Set (Var "o")) "," (Set ($#k3_semi_af1 :::"diff"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "o")) ")" ) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: SEMI_AF1:89 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool (Set (Var "o")) "," (Set ($#k3_semi_af1 :::"diff"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "o")) ")" ) "," (Set ($#k3_semi_af1 :::"diff"::: ) "(" (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "o")) ")" ) ($#r1_semi_af1 :::"is_collinear"::: ) ) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ))) ; definitionlet "SAS" be ($#l1_analoaf :::"Semi_Affine_Space":::); let "a", "b", "c", "d", "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SAS")); pred :::"trap"::: "a" "," "b" "," "c" "," "d" "," "o" means :: SEMI_AF1:def 8 (Bool "(" (Bool (Bool "not" "o" "," "a" "," "c" ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool "o" "," "a" "," "b" ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool "o" "," "c" "," "d" ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool "a" "," "c" ($#r2_analoaf :::"//"::: ) "b" "," "d") ")" ); end; :: deftheorem defines :::"trap"::: SEMI_AF1:def 8 : (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o"))) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ))); definitionlet "SAS" be ($#l1_analoaf :::"Semi_Affine_Space":::); let "o", "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SAS")); pred :::"qtrap"::: "o" "," "p" means :: SEMI_AF1:def 9 (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "SAS" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "SAS" "st" (Bool "(" (Bool (Bool "o" "," "p" "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "implies" (Bool "(" (Bool "o" "," (Set (Var "c")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool "p" "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ))); end; :: deftheorem defines :::"qtrap"::: SEMI_AF1:def 9 : (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds" (Bool "(" (Bool ($#r5_semi_af1 :::"qtrap"::: ) (Set (Var "o")) "," (Set (Var "p"))) "iff" (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool "(" (Bool (Bool (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) )) "implies" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ))) ")" ))); theorem :: SEMI_AF1:90 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")))) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "o"))) ")" ))) ; theorem :: SEMI_AF1:91 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "o")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "o"))) & (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "y")) "," (Set (Var "o")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: SEMI_AF1:92 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) ))) "holds" (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "o")) "," (Set (Var "o"))))) ; theorem :: SEMI_AF1:93 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")))) "holds" (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o"))))) ; theorem :: SEMI_AF1:94 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: SEMI_AF1:95 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")))) "holds" (Bool "not" (Bool (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "d")) ($#r1_semi_af1 :::"is_collinear"::: ) )))) ; theorem :: SEMI_AF1:96 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")))) "holds" (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "o"))))) ; theorem :: SEMI_AF1:97 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ; theorem :: SEMI_AF1:98 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "o"))) & (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "o")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "q")) "," (Set (Var "r"))))) ; theorem :: SEMI_AF1:99 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "o"))) & (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "o"))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) ))) "holds" (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "o"))))) ; theorem :: SEMI_AF1:100 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "d")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "o"))) & (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "o"))) & (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "d")) "," (Set (Var "s")) "," (Set (Var "o")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))))) ; theorem :: SEMI_AF1:101 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "p")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool ($#r5_semi_af1 :::"qtrap"::: ) (Set (Var "o")) "," (Set (Var "p"))) ")" )))) ; theorem :: SEMI_AF1:102 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "z"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" ))) ; theorem :: SEMI_AF1:103 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r5_semi_af1 :::"qtrap"::: ) (Set (Var "o")) "," (Set (Var "p")))) "holds" (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))))) ; theorem :: SEMI_AF1:104 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool ($#r5_semi_af1 :::"qtrap"::: ) (Set (Var "o")) "," (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "q")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool ($#r5_semi_af1 :::"qtrap"::: ) (Set (Var "o")) "," (Set (Var "q"))) ")" )))) ; theorem :: SEMI_AF1:105 (Bool "for" (Set (Var "SAS")) "being" ($#l1_analoaf :::"Semi_Affine_Space":::) (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "c")) ($#r1_semi_af1 :::"is_collinear"::: ) )) & (Bool (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "b")) ($#r1_semi_af1 :::"is_collinear"::: ) ) & (Bool ($#r5_semi_af1 :::"qtrap"::: ) (Set (Var "o")) "," (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st" (Bool ($#r4_semi_af1 :::"trap"::: ) (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")))))) ;