:: AFVECT01  semantic presentation begin  
















registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "C" be   ($#m1_subset_1 :::"Relation":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "A")) ($#k2_zfmisc_1 :::":]"::: ) ); 
cluster (Set   ($#g1_analoaf :::"AffinStruct"::: )  "(#"  "A" "," "C" "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_analoaf :::"AffinStruct"::: )  ; attr "IT" is  :::"WeakAffSegm-like":::  means :: AFVECT01: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")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (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 "c")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "a9"))) & (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "b9")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "or" (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st"  (Bool  "("  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))  ")" ) "or" (Bool  "ex" (Set (Var "p")) "," (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b")))  ")" ))  ")" ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "p")) "," (Set (Var "p9")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "b")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b9")) "," (Set (Var "c")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b9")) "," (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "p")) "," (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p9"))) & (Bool (Set (Var "b")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "b")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b9")))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "p9")) "," (Set (Var "q")) "," (Set (Var "q9")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "q")) "," (Set (Var "q9"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "q"))  ($#r2_analoaf :::"//"::: )  (Set (Var "q")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "q9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "q9")) "," (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "r")) "," (Set (Var "r9")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st"  (Bool  "("  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "r")) "," (Set (Var "r9"))) & (Bool (Set (Var "b")) "," (Set (Var "r"))  ($#r2_analoaf :::"//"::: )  (Set (Var "r")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "r9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "r9")) "," (Set (Var "c")))  ")" ))  ")" )  ")" ); end; 




:: deftheorem    defines :::"WeakAffSegm-like"::: AFVECT01: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_afvect01 :::"WeakAffSegm-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")) "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 "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (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 "c")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "a9"))) & (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "b9")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "or" (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))  ")" ) "or" (Bool  "ex" (Set (Var "p")) "," (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b")))  ")" ))  ")" ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "p")) "," (Set (Var "p9")) "," (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 "b")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "b")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b9")) "," (Set (Var "c")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b9")) "," (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "p")) "," (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p9"))) & (Bool (Set (Var "b")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "b")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b9")))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "p9")) "," (Set (Var "q")) "," (Set (Var "q9")) "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 "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "q")) "," (Set (Var "q9"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "q"))  ($#r2_analoaf :::"//"::: )  (Set (Var "q")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "q9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "q9")) "," (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "r")) "," (Set (Var "r9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "r")) "," (Set (Var "r9"))) & (Bool (Set (Var "b")) "," (Set (Var "r"))  ($#r2_analoaf :::"//"::: )  (Set (Var "r")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "r9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "r9")) "," (Set (Var "c")))  ")" ))  ")" )  ")" )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_analoaf :::"strict"::: )     ($#v1_afvect01 :::"WeakAffSegm-like"::: )    for    ($#l1_analoaf :::"AffinStruct"::: )  ; 
end; definitionmode WeakAffSegm is  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_afvect01 :::"WeakAffSegm-like"::: )     ($#l1_analoaf :::"AffinStruct"::: )  ; end; 













theorem :: AFVECT01:1 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "b"))))) ; 
 
theorem :: AFVECT01:2 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "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 :: AFVECT01:3 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "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 :: AFVECT01:4 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "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 :: AFVECT01:5 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds"  (Bool (Set (Var "a")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b"))))) ; 
 
theorem :: AFVECT01:6 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))) ; 
 
theorem :: AFVECT01:7 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "p9")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 
theorem :: AFVECT01:8 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b9")) "," (Set (Var "b99")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "b99"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "b99"))) & (Bool (Bool  "not" (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9")))) & (Bool (Bool  "not" (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b99"))))) "holds"  (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b99"))))) ; 
 definitionlet "AFV" be   ($#l1_analoaf :::"WeakAffSegm":::); let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); pred  :::"MDist"::: "a" "," "b" means :: AFVECT01:def 2 (Bool  "ex" (Set (Var "p")) "," (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AFV" "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p9"))) & (Bool "a" "," "b"  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool "a" "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," "b") & (Bool "a" "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," "b")  ")" )); end; 






:: deftheorem    defines :::"MDist"::: AFVECT01:def 2 :  (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds"   (Bool  "("  (Bool   ($#r1_afvect01 :::"MDist"::: )  (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "b")))  ")" ))  ")" ))); 
 definitionlet "AFV" be   ($#l1_analoaf :::"WeakAffSegm":::); let "a", "b", "c" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); pred  :::"Mid"::: "a" "," "b" "," "c" means :: AFVECT01:def 3 (Bool  "("  (Bool  "("  (Bool "a"  ($#r1_hidden :::"="::: )  "b") & (Bool "b"  ($#r1_hidden :::"="::: )  "c") & (Bool "a"  ($#r1_hidden :::"="::: )  "c")  ")" ) "or" (Bool  "("  (Bool "a"  ($#r1_hidden :::"="::: )  "c") & (Bool   ($#r1_afvect01 :::"MDist"::: )  "a" "," "b")  ")" ) "or" (Bool  "("  (Bool "a"  ($#r1_hidden :::"<>"::: )  "c") & (Bool "a" "," "b"  ($#r2_analoaf :::"//"::: )  "b" "," "c")  ")" )  ")" ); end; 







:: deftheorem    defines :::"Mid"::: AFVECT01:def 3 :  (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds"   (Bool  "("  (Bool   ($#r2_afvect01 :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool   ($#r1_afvect01 :::"MDist"::: )  (Set (Var "a")) "," (Set (Var "b")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))  ")" )  ")" )  ")" ))); 
 
theorem :: AFVECT01:9 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Bool  "not"   ($#r1_afvect01 :::"MDist"::: )  (Set (Var "a")) "," (Set (Var "b"))))) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))  ")" )))) ; 
 
theorem :: AFVECT01:10 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "st" (Bool (Bool   ($#r1_afvect01 :::"MDist"::: )  (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 
theorem :: AFVECT01:11 (Bool  "for" (Set (Var "AFV")) "being"   ($#l1_analoaf :::"WeakAffSegm":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV"))  "st" (Bool (Bool   ($#r1_afvect01 :::"MDist"::: )  (Set (Var "a")) "," (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))))) ;