:: COLLSP  semantic presentation begin  


definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; mode  :::"Relation3":::  "of" "X" ->    ($#m1_hidden :::"set"::: )   means :: COLLSP:def 1 (Bool it  ($#r1_tarski :::"c="::: )  (Set  ($#k3_zfmisc_1 :::"[:"::: ) "X" "," "X" "," "X" ($#k3_zfmisc_1 :::":]"::: ) )); end; 





:: deftheorem    defines :::"Relation3"::: COLLSP:def 1 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_collsp :::"Relation3"::: )   "of" (Set (Var "X"))) "iff" (Bool (Set (Var "b2"))  ($#r1_tarski :::"c="::: )  (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) "," (Set (Var "X")) ($#k3_zfmisc_1 :::":]"::: ) ))  ")" )); 
 
theorem :: COLLSP:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "X"))) "or" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ))  ")" ))  ")" )) ; 
 definitionattr "c1" is  :::"strict"::: ; struct  :::"CollStr":::  ->    ($#l1_struct_0 :::"1-sorted"::: )  ; aggr :::"CollStr":::(# :::"carrier":::, :::"Collinearity"::: #) ->    ($#l1_collsp :::"CollStr"::: )  ; sel  :::"Collinearity"::: "c1" ->    ($#m1_collsp :::"Relation3"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1"); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_collsp :::"strict"::: )    for    ($#l1_collsp :::"CollStr"::: )  ; 
end; 







definitionlet "CS" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_collsp :::"CollStr"::: )  ; let "a", "b", "c" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "CS")); pred "a" "," "b" "," "c" :::"is_collinear":::  means :: COLLSP:def 2 (Bool (Set  ($#k4_domain_1 :::"["::: ) "a" "," "b" "," "c" ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" "CS")); end; 







:: deftheorem    defines :::"is_collinear"::: COLLSP:def 2 :  (Bool  "for" (Set (Var "CS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_collsp :::"CollStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CS")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  ) "iff" (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" (Set (Var "CS"))))  ")" ))); 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_collsp :::"CollStr"::: )  ; attr "IT" is  :::"reflexive":::  means :: COLLSP:def 3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" "IT"  "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  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" "IT"))); end; 




:: deftheorem    defines :::"reflexive"::: COLLSP:def 3 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_collsp :::"CollStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_collsp :::"reflexive"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "IT"))  "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  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" (Set (Var "IT")))))  ")" )); 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_collsp :::"CollStr"::: )  ; attr "IT" is  :::"transitive":::  means :: COLLSP:def 4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" "IT"  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" "IT")) & (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" "IT")) & (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" "IT"))) "holds"  (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" "IT"))); end; 




:: deftheorem    defines :::"transitive"::: COLLSP:def 4 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_collsp :::"CollStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_collsp :::"transitive"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" (Set (Var "IT")))) & (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" (Set (Var "IT")))) & (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" (Set (Var "IT"))))) "holds"  (Bool (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k4_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_collsp :::"Collinearity"::: )  "of" (Set (Var "IT")))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_collsp :::"strict"::: )     ($#v2_collsp :::"reflexive"::: )     ($#v3_collsp :::"transitive"::: )    for    ($#l1_collsp :::"CollStr"::: )  ; 
end; definitionmode CollSp is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_collsp :::"reflexive"::: )     ($#v3_collsp :::"transitive"::: )     ($#l1_collsp :::"CollStr"::: )  ; end; 












theorem :: COLLSP:2 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "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")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: COLLSP:3 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: COLLSP:4 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_collsp :::"is_collinear"::: )  )  ")" ))) ; 
 
theorem :: COLLSP:5 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: COLLSP:6 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: COLLSP:7 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: COLLSP:8 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: COLLSP:9 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 definitionlet "CLSP" be   ($#l1_collsp :::"CollSp":::); let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "CLSP")); func  :::"Line":::  "(" "a" "," "b" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: COLLSP:def 5  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" "CLSP" : (Bool "a" "," "b" "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  )  "}"  ; end; 







:: deftheorem    defines :::"Line"::: COLLSP:def 5 :  (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) "holds"  (Bool (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) : (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  )  "}"  ))); 
 
theorem :: COLLSP:10 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" ))) ; 
 
theorem :: COLLSP:11 (Bool  "for" (Set (Var "CLSP")) "being"   ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ) "iff" (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" ))) ; 
 




definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_collsp :::"CollStr"::: )  ; attr "IT" is  :::"proper":::  means :: COLLSP:def 6 (Bool  "not" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" "IT" "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  ))); end; 




:: deftheorem    defines :::"proper"::: COLLSP:def 6 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_collsp :::"CollStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_collsp :::"proper"::: )  ) "iff" (Bool  "not" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_collsp :::"strict"::: )     ($#v2_collsp :::"reflexive"::: )     ($#v3_collsp :::"transitive"::: )     ($#v4_collsp :::"proper"::: )    for    ($#l1_collsp :::"CollStr"::: )  ; 
end; 











theorem :: COLLSP:12 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) "st" (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))))) ; 
 definitionlet "CLSP" be   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::); mode  :::"LINE":::  "of" "CLSP" ->    ($#m1_hidden :::"set"::: )   means :: COLLSP:def 7 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" "CLSP" "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" )); end; 





:: deftheorem    defines :::"LINE"::: COLLSP:def 7 :  (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP"))) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" ))  ")" ))); 
 




theorem :: COLLSP:13 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "CLSP")))))) ; 
 
theorem :: COLLSP:14 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "P")) "being"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP")) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: COLLSP:15 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "P")) "being"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: COLLSP:16 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  )))) ; 
 
theorem :: COLLSP:17 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "P"))  ($#r1_tarski :::"c="::: )  (Set (Var "Q")))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q"))))) ; 
 
theorem :: COLLSP:18 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "P")))))) ; 
 
theorem :: COLLSP:19 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "P")))))) ; 
 
theorem :: COLLSP:20 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "Q"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "Q")))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))))) ; 
 
theorem :: COLLSP:21 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"    ($#m2_collsp :::"LINE"::: )   "of" (Set (Var "CLSP"))  "holds"  (Bool  "("  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q"))) "or" (Bool (Set (Var "P"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Q"))) "or" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP")) "st" (Bool (Set (Set (Var "P"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Q")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )))  ")" ))) ; 
 
theorem :: COLLSP:22 (Bool  "for" (Set (Var "CLSP")) "being"   ($#v4_collsp :::"proper"::: )    ($#l1_collsp :::"CollSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CLSP"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k1_collsp :::"Line"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"<>"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "CLSP")))))) ;