:: COLLSP semantic presentation

begin

definition
let X be ( ( ) ( ) set ) ;
mode Relation3 of X -> ( ( ) ( ) set ) means :: COLLSP:def 1
it : ( ( ) ( ) set ) c= [:X : ( ( ) ( ) 2-sorted ) ,X : ( ( ) ( ) 2-sorted ) ,X : ( ( ) ( ) 2-sorted ) :] : ( ( ) ( ) set ) ;
end;

theorem :: COLLSP:1
for X being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) = {} : ( ( ) ( empty V17() V18() V19() V21() V22() V23() ) set ) or ex a being ( ( ) ( ) set ) st
( {a : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) = X : ( ( ) ( ) set ) or ex a, b being ( ( ) ( ) set ) st
( a : ( ( ) ( ) set ) <> b : ( ( ) ( ) set ) & a : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ) ) ;

definition
attr c1 is strict ;
struct CollStr -> ( ( ) ( ) 1-sorted ) ;
aggr CollStr(# carrier, Collinearity #) -> ( ( strict ) ( strict ) CollStr ) ;
sel Collinearity c1 -> ( ( ) ( ) Relation3 of the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster non empty strict for ( ( ) ( ) CollStr ) ;
end;

definition
let CS be ( ( non empty ) ( non empty ) CollStr ) ;
let a, b, c be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
pred a,b,c is_collinear means :: COLLSP:def 2
[a : ( ( ) ( ) set ) ,b : ( ( ) ( ) Element of CS : ( ( ) ( ) 2-sorted ) ) ,c : ( ( ) ( ) Element of CS : ( ( ) ( ) 2-sorted ) ) ] : ( ( ) ( ) Element of [: the carrier of CS : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of CS : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of CS : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in the Collinearity of CS : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) Relation3 of the carrier of CS : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ;
end;

definition
let IT be ( ( non empty ) ( non empty ) CollStr ) ;
attr IT is reflexive means :: COLLSP:def 3
 for a, b, c being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st ( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) or b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds
[a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in the Collinearity of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) Relation3 of the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ;
end;

definition
let IT be ( ( non empty ) ( non empty ) CollStr ) ;
attr IT is transitive means :: COLLSP:def 4
 for a, b, p, q, r being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & [a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in the Collinearity of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) Relation3 of the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) & [a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in the Collinearity of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) Relation3 of the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) & [a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in the Collinearity of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) Relation3 of the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) holds
[p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) in the Collinearity of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) Relation3 of the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster non empty strict reflexive transitive for ( ( ) ( ) CollStr ) ;
end;

definition
mode CollSp is ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollStr ) ;
end;

theorem :: COLLSP:2
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b, c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st ( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) or b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds
a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

theorem :: COLLSP:3
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b, p, q, r being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear holds
p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

theorem :: COLLSP:4
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b, c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear holds
( b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ) ;

theorem :: COLLSP:5
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

theorem :: COLLSP:6
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b, c, d being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear holds
a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

theorem :: COLLSP:7
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b, c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear holds
b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

theorem :: COLLSP:8
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b, c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear holds
b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

theorem :: COLLSP:9
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for p, q, a, b, r being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear & p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear holds
a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

definition
let CLSP be ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp) ;
let a, b be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
func Line (a,b) -> ( ( ) ( ) set ) equals :: COLLSP:def 5
 { p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( ) Point of ( ( ) ( ) set ) ) : a : ( ( ) ( ) set ) ,b : ( ( ) ( ) Element of CLSP : ( ( ) ( ) 2-sorted ) ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear } ;
end;

theorem :: COLLSP:10
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Line (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Line (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: COLLSP:11
for CLSP being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) CollSp)
for a, b, r being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear iff r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Line (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) CollStr ) ;
attr IT is proper means :: COLLSP:def 6
 not for a, b, c being ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;
end;

registration
cluster non empty strict reflexive transitive proper for ( ( ) ( ) CollStr ) ;
end;

theorem :: COLLSP:12
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
ex r being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st not p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

definition
let CLSP be ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ;
mode LINE of CLSP -> ( ( ) ( ) set ) means :: COLLSP:def 7
 ex a, b being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & it : ( ( ) ( ) set ) = Line (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) );
end;

theorem :: COLLSP:13
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
Line (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = the carrier of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) : ( ( ) ( non empty ) set ) ;

theorem :: COLLSP:14
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for P being ( ( ) ( ) LINE of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) ex a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) ) ;

theorem :: COLLSP:15
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
ex P being ( ( ) ( ) LINE of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) st
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) ) ;

theorem :: COLLSP:16
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for p, q, r being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( ) LINE of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) holds
p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_collinear ;

theorem :: COLLSP:17
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for P, Q being ( ( ) ( ) LINE of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) st P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) c= Q : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) holds
P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) = Q : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) ;

theorem :: COLLSP:18
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( ) LINE of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) holds
Line (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) c= P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) ;

theorem :: COLLSP:19
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( ) LINE of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) holds
Line (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) ;

theorem :: COLLSP:20
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( ) LINE of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Q : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) & q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Q : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) holds
P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) = Q : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) ;

theorem :: COLLSP:21
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for P, Q being ( ( ) ( ) LINE of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) holds
( P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) = Q : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) or P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) misses Q : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) or ex p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st P : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) /\ Q : ( ( ) ( ) LINE of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) ) : ( ( ) ( ) set ) = {p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: COLLSP:22
for CLSP being ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
Line (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) <> the carrier of CLSP : ( ( non empty reflexive transitive proper ) ( non empty reflexive transitive proper ) CollSp) : ( ( ) ( non empty ) set ) ;