:: COLLSP semantic presentation

begin

definition
let X be set ;
mode Relation3 of X ->  set  means :Def1: :: COLLSP:def 1
it c= [:X,X,X:];
existence
 ex b1 being set st b1 c= [:X,X,X:] ;
end;

:: deftheorem Def1 defines Relation3 COLLSP:def_1_:_
 for X, b2 being set holds
( b2 is Relation3 of X iff b2 c= [:X,X,X:] );

theorem Th1: :: COLLSP:1
for X being set holds
( X = {} or ex a being set st
( {a} = X or ex a, b being set st
( a <> b & a in X & b in X ) ) )
proof
let X be set ; ::_thesis: ( X = {} or ex a being set st
( {a} = X or ex a, b being set st
( a <> b & a in X & b in X ) ) )
now__::_thesis:_(_X_<>_{}_&_(_for_a,_b_being_set_holds_
(_not_a_<>_b_or_not_a_in_X_or_not_b_in_X_)_)_implies_ex_a_being_set_st_{a}_=_X_)
set p = the Element of X;
assume  ( X <> {} & ( for a, b being set holds
( not a <> b or not a in X or not b in X ) ) ) ; ::_thesis: ex a being set st {a} = X
then  for z being set holds
( z in X iff z = the Element of X ) ;
then  X = { the Element of X} by TARSKI:def_1;
hence  ex a being set st {a} = X ; ::_thesis: verum
end;
hence  ( X = {} or ex a being set st
( {a} = X or ex a, b being set st
( a <> b & a in X & b in X ) ) ) ; ::_thesis: verum
end;

definition
attrc1 is strict ;
struct CollStr  ->  1-sorted ;
aggrCollStr(# carrier, Collinearity #) ->  CollStr ;
sel Collinearity c1 ->  Relation3 of the carrier of c1;
end;

registration
cluster non empty strict for CollStr ;
existence
 ex b1 being CollStr st
( not b1 is empty & b1 is strict )
proof
set A = the non empty set ;
set r = the Relation3 of the non empty set ;
take  CollStr(# the non empty set , the Relation3 of the non empty set #) ; ::_thesis: ( not CollStr(# the non empty set , the Relation3 of the non empty set #) is empty & CollStr(# the non empty set , the Relation3 of the non empty set #) is strict )
thus  not the carrier of CollStr(# the non empty set , the Relation3 of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: CollStr(# the non empty set , the Relation3 of the non empty set #) is strict
thus  CollStr(# the non empty set , the Relation3 of the non empty set #) is strict ; ::_thesis: verum
end;
end;


definition
let CS be non empty CollStr ;
let a, b, c be Point of CS;
preda,b,c is_collinear  means :Def2: :: COLLSP:def 2
[a,b,c] in the Collinearity of CS;
end;

:: deftheorem Def2 defines is_collinear COLLSP:def_2_:_
 for CS being non empty CollStr
for a, b, c being Point of CS holds
( a,b,c is_collinear iff [a,b,c] in the Collinearity of CS );

set Z = {1};

Lm1:  1 in {1}
by TARSKI:def_1;

Lm2:  {[1,1,1]} c= [:{1},{1},{1}:]
proof
now__::_thesis:_for_x_being_set_st_x_in_{[1,1,1]}_holds_
x_in_[:{1},{1},{1}:]
let x be set ; ::_thesis: ( x in {[1,1,1]} implies x in [:{1},{1},{1}:] )
assume  x in {[1,1,1]} ; ::_thesis: x in [:{1},{1},{1}:]
then  x = [1,1,1] by TARSKI:def_1;
hence  x in [:{1},{1},{1}:] by Lm1, MCART_1:69; ::_thesis: verum
end;
hence  {[1,1,1]} c= [:{1},{1},{1}:] by TARSKI:def_3; ::_thesis: verum
end;

reconsider Z = {1} as non empty set ;

reconsider RR = {[1,1,1]} as Relation3 of Z by Def1, Lm2;

reconsider CLS = CollStr(# Z,RR #) as non empty CollStr ;

Lm3: now__::_thesis:_for_a,_b,_c,_p,_q,_r_being_Point_of_CLS_holds_
(_(_(_a_=_b_or_a_=_c_or_b_=_c_)_implies_[a,b,c]_in_the_Collinearity_of_CLS_)_&_(_a_<>_b_&_[a,b,p]_in_the_Collinearity_of_CLS_&_[a,b,q]_in_the_Collinearity_of_CLS_&_[a,b,r]_in_the_Collinearity_of_CLS_implies_[p,q,r]_in_the_Collinearity_of_CLS_)_)
let a, b, c, p, q, r be Point of CLS; ::_thesis: ( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) & ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) )
A1: for z1, z2, z3 being Point of CLS holds [z1,z2,z3] in the Collinearity of CLS
proof
let z1, z2, z3 be Point of CLS; ::_thesis: [z1,z2,z3] in the Collinearity of CLS
A2: z3 = 1 by TARSKI:def_1;
 ( z1 = 1 & z2 = 1 ) by TARSKI:def_1;
hence  [z1,z2,z3] in the Collinearity of CLS by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) ; ::_thesis: ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS )
thus  ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) by A1; ::_thesis: verum
end;

definition
let IT be non empty CollStr ;
attrIT is reflexive  means :Def3: :: COLLSP:def 3
 for a, b, c being Point of IT st ( a = b or a = c or b = c ) holds
[a,b,c] in the Collinearity of IT;
end;

:: deftheorem Def3 defines reflexive COLLSP:def_3_:_
 for IT being non empty CollStr holds
( IT is reflexive iff for a, b, c being Point of IT st ( a = b or a = c or b = c ) holds
[a,b,c] in the Collinearity of IT );

definition
let IT be non empty CollStr ;
attrIT is transitive  means :Def4: :: COLLSP:def 4
 for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds
[p,q,r] in the Collinearity of IT;
end;

:: deftheorem Def4 defines transitive COLLSP:def_4_:_
 for IT being non empty CollStr holds
( IT is transitive iff for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds
[p,q,r] in the Collinearity of IT );

registration
cluster non empty strict reflexive transitive for CollStr ;
existence
 ex b1 being non empty CollStr st
( b1 is strict & b1 is reflexive & b1 is transitive )
proof
take  CLS ; ::_thesis: ( CLS is strict & CLS is reflexive & CLS is transitive )
thus  ( CLS is strict & CLS is reflexive & CLS is transitive ) by Def3, Def4, Lm3; ::_thesis: verum
end;
end;

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


theorem Th2: :: COLLSP:2
for CLSP being CollSp
for a, b, c being Point of CLSP st ( a = b or a = c or b = c ) holds
a,b,c is_collinear
proof
let CLSP be CollSp; ::_thesis: for a, b, c being Point of CLSP st ( a = b or a = c or b = c ) holds
a,b,c is_collinear
let a, b, c be Point of CLSP; ::_thesis: ( ( a = b or a = c or b = c ) implies a,b,c is_collinear )
assume  ( a = b or a = c or b = c ) ; ::_thesis: a,b,c is_collinear
then  [a,b,c] in the Collinearity of CLSP by Def3;
hence  a,b,c is_collinear by Def2; ::_thesis: verum
end;

theorem Th3: :: COLLSP:3
for CLSP being CollSp
for a, b, p, q, r being Point of CLSP st a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear holds
p,q,r is_collinear
proof
let CLSP be CollSp; ::_thesis: for a, b, p, q, r being Point of CLSP st a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear holds
p,q,r is_collinear
let a, b, p, q, r be Point of CLSP; ::_thesis: ( a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear implies p,q,r is_collinear )
assume that
A1: a <> b and
A2: ( a,b,p is_collinear & a,b,q is_collinear ) and
A3: a,b,r is_collinear ; ::_thesis: p,q,r is_collinear
A4: [a,b,r] in the Collinearity of CLSP by A3, Def2;
 ( [a,b,p] in the Collinearity of CLSP & [a,b,q] in the Collinearity of CLSP ) by A2, Def2;
then  [p,q,r] in the Collinearity of CLSP by A1, A4, Def4;
hence  p,q,r is_collinear by Def2; ::_thesis: verum
end;

theorem Th4: :: COLLSP:4
for CLSP being CollSp
for a, b, c being Point of CLSP st a,b,c is_collinear holds
( b,a,c is_collinear & a,c,b is_collinear )
proof
let CLSP be CollSp; ::_thesis: for a, b, c being Point of CLSP st a,b,c is_collinear holds
( b,a,c is_collinear & a,c,b is_collinear )
let a, b, c be Point of CLSP; ::_thesis: ( a,b,c is_collinear implies ( b,a,c is_collinear & a,c,b is_collinear ) )
assume A1: a,b,c is_collinear ; ::_thesis: ( b,a,c is_collinear & a,c,b is_collinear )
then  ( a = b or ( a <> b & a,b,b is_collinear & a,b,a is_collinear & a,b,c is_collinear ) ) by Th2;
hence  b,a,c is_collinear by Th2, Th3; ::_thesis: a,c,b is_collinear
 ( a = b or ( a <> b & a,b,a is_collinear & a,b,c is_collinear & a,b,b is_collinear ) ) by A1, Th2;
hence  a,c,b is_collinear by Th2, Th3; ::_thesis: verum
end;

theorem :: COLLSP:5
for CLSP being CollSp
for a, b being Point of CLSP holds a,b,a is_collinear by Th2;

theorem Th6: :: COLLSP:6
for CLSP being CollSp
for a, b, c, d being Point of CLSP st a <> b & a,b,c is_collinear & a,b,d is_collinear holds
a,c,d is_collinear
proof
let CLSP be CollSp; ::_thesis: for a, b, c, d being Point of CLSP st a <> b & a,b,c is_collinear & a,b,d is_collinear holds
a,c,d is_collinear
let a, b, c, d be Point of CLSP; ::_thesis: ( a <> b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear )
assume A1: ( a <> b & a,b,c is_collinear & a,b,d is_collinear ) ; ::_thesis: a,c,d is_collinear
 a,b,a is_collinear by Th2;
hence  a,c,d is_collinear by A1, Th3; ::_thesis: verum
end;

theorem :: COLLSP:7
for CLSP being CollSp
for a, b, c being Point of CLSP st a,b,c is_collinear holds
b,a,c is_collinear by Th4;

theorem Th8: :: COLLSP:8
for CLSP being CollSp
for a, b, c being Point of CLSP st a,b,c is_collinear holds
b,c,a is_collinear
proof
let CLSP be CollSp; ::_thesis: for a, b, c being Point of CLSP st a,b,c is_collinear holds
b,c,a is_collinear
let a, b, c be Point of CLSP; ::_thesis: ( a,b,c is_collinear implies b,c,a is_collinear )
assume  a,b,c is_collinear ; ::_thesis: b,c,a is_collinear
then  b,a,c is_collinear by Th4;
hence  b,c,a is_collinear by Th4; ::_thesis: verum
end;

theorem Th9: :: COLLSP:9
for CLSP being CollSp
for p, q, a, b, r being Point of CLSP st p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear holds
a,b,r is_collinear
proof
let CLSP be CollSp; ::_thesis: for p, q, a, b, r being Point of CLSP st p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear holds
a,b,r is_collinear
let p, q, a, b, r be Point of CLSP; ::_thesis: ( p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear implies a,b,r is_collinear )
assume that
A1: p <> q and
A2: ( a,b,p is_collinear & a,b,q is_collinear ) and
A3: p,q,r is_collinear ; ::_thesis: a,b,r is_collinear
now__::_thesis:_(_a_<>_b_implies_a,b,r_is_collinear_)
assume A4: a <> b ; ::_thesis: a,b,r is_collinear
then  a,p,q is_collinear by A2, Th6;
then A5: p,q,a is_collinear by Th8;
 a,b,b is_collinear by Th2;
then  p,q,b is_collinear by A2, A4, Th3;
hence  a,b,r is_collinear by A1, A3, A5, Th3; ::_thesis: verum
end;
hence  a,b,r is_collinear by Th2; ::_thesis: verum
end;

definition
let CLSP be CollSp;
let a, b be Point of CLSP;
func Line (a,b) ->  set  equals :: COLLSP:def 5
 {  p where p is Point of CLSP : a,b,p is_collinear  }  ;
correctness
coherence
{  p where p is Point of CLSP : a,b,p is_collinear  }  is set ;
;
end;

:: deftheorem  defines Line COLLSP:def_5_:_
 for CLSP being CollSp
for a, b being Point of CLSP holds Line (a,b) =  {  p where p is Point of CLSP : a,b,p is_collinear  }  ;

theorem Th10: :: COLLSP:10
for CLSP being CollSp
for a, b being Point of CLSP holds
( a in Line (a,b) & b in Line (a,b) )
proof
let CLSP be CollSp; ::_thesis: for a, b being Point of CLSP holds
( a in Line (a,b) & b in Line (a,b) )
let a, b be Point of CLSP; ::_thesis: ( a in Line (a,b) & b in Line (a,b) )
 a,b,a is_collinear by Th2;
hence  a in Line (a,b) ; ::_thesis: b in Line (a,b)
 a,b,b is_collinear by Th2;
hence  b in Line (a,b) ; ::_thesis: verum
end;

theorem Th11: :: COLLSP:11
for CLSP being CollSp
for a, b, r being Point of CLSP holds
( a,b,r is_collinear iff r in Line (a,b) )
proof
let CLSP be CollSp; ::_thesis: for a, b, r being Point of CLSP holds
( a,b,r is_collinear iff r in Line (a,b) )
let a, b, r be Point of CLSP; ::_thesis: ( a,b,r is_collinear iff r in Line (a,b) )
thus  ( a,b,r is_collinear implies r in Line (a,b) ) ; ::_thesis: ( r in Line (a,b) implies a,b,r is_collinear )
thus  ( r in Line (a,b) implies a,b,r is_collinear ) ::_thesis: verum
proof
assume  r in Line (a,b) ; ::_thesis: a,b,r is_collinear
then  ex p being Point of CLSP st
( r = p & a,b,p is_collinear ) ;
hence  a,b,r is_collinear ; ::_thesis: verum
end;
end;

   set Z = {1,2,3};

set RR =  {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} )  }  ;

Lm4:   {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} )  }  c= [:{1,2,3},{1,2,3},{1,2,3}:]
proof
now__::_thesis:_for_x_being_set_st_x_in__{__[i,j,k]_where_i,_j,_k_is_Element_of_NAT_:_(_(_i_=_j_or_j_=_k_or_k_=_i_)_&_i_in_{1,2,3}_&_j_in_{1,2,3}_&_k_in_{1,2,3}_)__}__holds_
x_in_[:{1,2,3},{1,2,3},{1,2,3}:]
let x be set ; ::_thesis: ( x in  {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} )  }  implies x in [:{1,2,3},{1,2,3},{1,2,3}:] )
assume  x in  {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} )  }  ; ::_thesis: x in [:{1,2,3},{1,2,3},{1,2,3}:]
then  ex i, j, k being Element of NAT st
( x = [i,j,k] & ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) ;
hence  x in [:{1,2,3},{1,2,3},{1,2,3}:] by MCART_1:69; ::_thesis: verum
end;
hence   {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} )  }  c= [:{1,2,3},{1,2,3},{1,2,3}:] by TARSKI:def_3; ::_thesis: verum
end;

reconsider Z = {1,2,3} as non empty set by ENUMSET1:def_1;

reconsider RR =  {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} )  }  as Relation3 of Z by Def1, Lm4;

reconsider CLS = CollStr(# Z,RR #) as non empty CollStr ;

Lm5:  for a, b, c being Point of CLS holds
( [a,b,c] in RR iff ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) )
proof
let a, b, c be Point of CLS; ::_thesis: ( [a,b,c] in RR iff ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) )
thus  ( [a,b,c] in RR implies ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) ) ::_thesis: ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z implies [a,b,c] in RR )
proof
assume  [a,b,c] in RR ; ::_thesis: ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z )
then consider i, j, k being Element of NAT  such that
A1: [a,b,c] = [i,j,k] and
A2: ( i = j or j = k or k = i ) and
 i in Z and
 j in Z and
 k in Z ;
 ( a = i & b = j ) by A1, XTUPLE_0:3;
hence  ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) by A1, A2, XTUPLE_0:3; ::_thesis: verum
end;
thus  ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z implies [a,b,c] in RR ) ; ::_thesis: verum
end;

Lm6:  for a, b, c, p, q, r being Point of CLS st a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS holds
[p,q,r] in the Collinearity of CLS
proof
let a, b, c, p, q, r be Point of CLS; ::_thesis: ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS )
assume that
A1: a <> b and
A2: [a,b,p] in the Collinearity of CLS and
A3: [a,b,q] in the Collinearity of CLS and
A4: [a,b,r] in the Collinearity of CLS ; ::_thesis: [p,q,r] in the Collinearity of CLS
A5: ( a = q or b = q ) by A1, A3, Lm5;
A6: ( a = r or b = r ) by A1, A4, Lm5;
A7: ( p in Z & q in Z ) ;
A8: r in Z ;
 ( a = p or b = p ) by A1, A2, Lm5;
hence  [p,q,r] in the Collinearity of CLS by A5, A6, A7, A8; ::_thesis: verum
end;

Lm7:  not for a, b, c being Point of CLS holds a,b,c is_collinear
proof
reconsider a = 1, b = 2, c = 3 as Point of CLS by ENUMSET1:def_1;
take  a ; ::_thesis: not for b, c being Point of CLS holds a,b,c is_collinear
take  b ; ::_thesis: not for c being Point of CLS holds a,b,c is_collinear
take  c ; ::_thesis: not a,b,c is_collinear
 not [a,b,c] in the Collinearity of CLS by Lm5;
hence  not a,b,c is_collinear by Def2; ::_thesis: verum
end;

Lm8:  CLS is CollSp
proof
 for a, b, c, p, q, r being Point of CLS holds
( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) & ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) ) by Lm5, Lm6;
hence  CLS is CollSp by Def3, Def4; ::_thesis: verum
end;

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

:: deftheorem Def6 defines proper COLLSP:def_6_:_
 for IT being non empty CollStr holds
( IT is proper iff not for a, b, c being Point of IT holds a,b,c is_collinear );

registration
cluster non empty strict reflexive transitive proper for CollStr ;
existence
 ex b1 being CollSp st
( b1 is strict & b1 is proper )
proof
reconsider CLS = CLS as CollSp by Lm8;
 CLS is proper by Def6, Lm7;
hence  ex b1 being CollSp st
( b1 is strict & b1 is proper ) ; ::_thesis: verum
end;
end;


theorem Th12: :: COLLSP:12
for CLSP being proper CollSp
for p, q being Point of CLSP st p <> q holds
ex r being Point of CLSP st not p,q,r is_collinear
proof
let CLSP be proper CollSp; ::_thesis: for p, q being Point of CLSP st p <> q holds
ex r being Point of CLSP st not p,q,r is_collinear
let p, q be Point of CLSP; ::_thesis: ( p <> q implies ex r being Point of CLSP st not p,q,r is_collinear )
consider a, b, c being Point of CLSP such that
A1: not a,b,c is_collinear by Def6;
assume  p <> q ; ::_thesis: not for r being Point of CLSP holds p,q,r is_collinear
then  ( not p,q,a is_collinear or not p,q,b is_collinear or not p,q,c is_collinear ) by A1, Th3;
hence  not for r being Point of CLSP holds p,q,r is_collinear ; ::_thesis: verum
end;

definition
let CLSP be proper CollSp;
mode LINE of CLSP ->  set  means :Def7: :: COLLSP:def 7
 ex a, b being Point of CLSP st
( a <> b & it = Line (a,b) );
existence
 ex b1 being set ex a, b being Point of CLSP st
( a <> b & b1 = Line (a,b) )
proof
consider a, b, c being Point of CLSP such that
A1: not a,b,c is_collinear by Def6;
take  Line (a,b) ; ::_thesis: ex a, b being Point of CLSP st
( a <> b & Line (a,b) = Line (a,b) )
 a <> b by A1, Th2;
hence  ex a, b being Point of CLSP st
( a <> b & Line (a,b) = Line (a,b) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines LINE COLLSP:def_7_:_
 for CLSP being proper CollSp
for b2 being set holds
( b2 is LINE of CLSP iff ex a, b being Point of CLSP st
( a <> b & b2 = Line (a,b) ) );


theorem :: COLLSP:13
for CLSP being proper CollSp
for a, b being Point of CLSP st a = b holds
Line (a,b) = the carrier of CLSP
proof
let CLSP be proper CollSp; ::_thesis: for a, b being Point of CLSP st a = b holds
Line (a,b) = the carrier of CLSP
let a, b be Point of CLSP; ::_thesis: ( a = b implies Line (a,b) = the carrier of CLSP )
assume A1: a = b ; ::_thesis: Line (a,b) = the carrier of CLSP
 for x being set holds
( x in Line (a,b) iff x in the carrier of CLSP )
proof
let x be set ; ::_thesis: ( x in Line (a,b) iff x in the carrier of CLSP )
thus  ( x in Line (a,b) implies x in the carrier of CLSP ) ::_thesis: ( x in the carrier of CLSP implies x in Line (a,b) )
proof
assume  x in Line (a,b) ; ::_thesis: x in the carrier of CLSP
then  ex p being Point of CLSP st
( x = p & a,b,p is_collinear ) ;
then reconsider x = x as Point of CLSP ;
 x is Element of CLSP ;
hence  x in the carrier of CLSP ; ::_thesis: verum
end;
thus  ( x in the carrier of CLSP implies x in Line (a,b) ) ::_thesis: verum
proof
assume  x in the carrier of CLSP ; ::_thesis: x in Line (a,b)
then reconsider x = x as Point of CLSP ;
 a,b,x is_collinear by A1, Th2;
hence  x in Line (a,b) ; ::_thesis: verum
end;
end;
hence  Line (a,b) = the carrier of CLSP by TARSKI:1; ::_thesis: verum
end;

theorem :: COLLSP:14
for CLSP being proper CollSp
for P being LINE of CLSP ex a, b being Point of CLSP st
( a <> b & a in P & b in P )
proof
let CLSP be proper CollSp; ::_thesis: for P being LINE of CLSP ex a, b being Point of CLSP st
( a <> b & a in P & b in P )
let P be LINE of CLSP; ::_thesis: ex a, b being Point of CLSP st
( a <> b & a in P & b in P )
consider a, b being Point of CLSP such that
A1: ( a <> b & P = Line (a,b) ) by Def7;
take  a ; ::_thesis: ex b being Point of CLSP st
( a <> b & a in P & b in P )
take  b ; ::_thesis: ( a <> b & a in P & b in P )
thus  ( a <> b & a in P & b in P ) by A1, Th10; ::_thesis: verum
end;

theorem :: COLLSP:15
for CLSP being proper CollSp
for a, b being Point of CLSP st a <> b holds
ex P being LINE of CLSP st
( a in P & b in P )
proof
let CLSP be proper CollSp; ::_thesis: for a, b being Point of CLSP st a <> b holds
ex P being LINE of CLSP st
( a in P & b in P )
let a, b be Point of CLSP; ::_thesis: ( a <> b implies ex P being LINE of CLSP st
( a in P & b in P ) )
assume  a <> b ; ::_thesis: ex P being LINE of CLSP st
( a in P & b in P )
then reconsider P = Line (a,b) as LINE of CLSP by Def7;
take  P ; ::_thesis: ( a in P & b in P )
thus  ( a in P & b in P ) by Th10; ::_thesis: verum
end;

theorem Th16: :: COLLSP:16
for CLSP being proper CollSp
for p, q, r being Point of CLSP
for P being LINE of CLSP st p in P & q in P & r in P holds
p,q,r is_collinear
proof
let CLSP be proper CollSp; ::_thesis: for p, q, r being Point of CLSP
for P being LINE of CLSP st p in P & q in P & r in P holds
p,q,r is_collinear
let p, q, r be Point of CLSP; ::_thesis: for P being LINE of CLSP st p in P & q in P & r in P holds
p,q,r is_collinear
let P be LINE of CLSP; ::_thesis: ( p in P & q in P & r in P implies p,q,r is_collinear )
assume that
A1: ( p in P & q in P ) and
A2: r in P ; ::_thesis: p,q,r is_collinear
consider a, b being Point of CLSP such that
A3: a <> b and
A4: P = Line (a,b) by Def7;
A5: ex z being Point of CLSP st
( z = r & a,b,z is_collinear ) by A2, A4;
 ( ex x being Point of CLSP st
( x = p & a,b,x is_collinear ) & ex y being Point of CLSP st
( y = q & a,b,y is_collinear ) ) by A1, A4;
hence  p,q,r is_collinear by A3, A5, Th3; ::_thesis: verum
end;

Lm9:  for CLSP being proper CollSp
for P being LINE of CLSP
for x being set st x in P holds
x is Point of CLSP
proof
let CLSP be proper CollSp; ::_thesis: for P being LINE of CLSP
for x being set st x in P holds
x is Point of CLSP
let P be LINE of CLSP; ::_thesis: for x being set st x in P holds
x is Point of CLSP
let x be set ; ::_thesis: ( x in P implies x is Point of CLSP )
consider a, b being Point of CLSP such that
 a <> b and
A1: P = Line (a,b) by Def7;
assume  x in P ; ::_thesis: x is Point of CLSP
then  ex r being Point of CLSP st
( r = x & a,b,r is_collinear ) by A1;
hence  x is Point of CLSP ; ::_thesis: verum
end;

theorem Th17: :: COLLSP:17
for CLSP being proper CollSp
for P, Q being LINE of CLSP st P c= Q holds
P = Q
proof
let CLSP be proper CollSp; ::_thesis: for P, Q being LINE of CLSP st P c= Q holds
P = Q
let P, Q be LINE of CLSP; ::_thesis: ( P c= Q implies P = Q )
assume A1: P c= Q ; ::_thesis: P = Q
 Q c= P
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in Q or r in P )
consider p, q being Point of CLSP such that
 p <> q and
A2: P = Line (p,q) by Def7;
assume A3: r in Q ; ::_thesis: r in P
then reconsider r = r as Point of CLSP by Lm9;
 ( p in P & q in P ) by A2, Th10;
then  p,q,r is_collinear by A1, A3, Th16;
hence  r in P by A2; ::_thesis: verum
end;
hence  P = Q by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th18: :: COLLSP:18
for CLSP being proper CollSp
for p, q being Point of CLSP
for P being LINE of CLSP st p <> q & p in P & q in P holds
Line (p,q) c= P
proof
let CLSP be proper CollSp; ::_thesis: for p, q being Point of CLSP
for P being LINE of CLSP st p <> q & p in P & q in P holds
Line (p,q) c= P
let p, q be Point of CLSP; ::_thesis: for P being LINE of CLSP st p <> q & p in P & q in P holds
Line (p,q) c= P
let P be LINE of CLSP; ::_thesis: ( p <> q & p in P & q in P implies Line (p,q) c= P )
assume that
A1: p <> q and
A2: ( p in P & q in P ) ; ::_thesis: Line (p,q) c= P
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Line (p,q) or x in P )
consider a, b being Point of CLSP such that
 a <> b and
A3: P = Line (a,b) by Def7;
assume  x in Line (p,q) ; ::_thesis: x in P
then consider r being Point of CLSP such that
A4: r = x and
A5: p,q,r is_collinear ;
 ( a,b,p is_collinear & a,b,q is_collinear ) by A2, A3, Th11;
then  a,b,r is_collinear by A1, A5, Th9;
hence  x in P by A3, A4; ::_thesis: verum
end;

theorem Th19: :: COLLSP:19
for CLSP being proper CollSp
for p, q being Point of CLSP
for P being LINE of CLSP st p <> q & p in P & q in P holds
Line (p,q) = P
proof
let CLSP be proper CollSp; ::_thesis: for p, q being Point of CLSP
for P being LINE of CLSP st p <> q & p in P & q in P holds
Line (p,q) = P
let p, q be Point of CLSP; ::_thesis: for P being LINE of CLSP st p <> q & p in P & q in P holds
Line (p,q) = P
let P be LINE of CLSP; ::_thesis: ( p <> q & p in P & q in P implies Line (p,q) = P )
assume that
A1: p <> q and
A2: ( p in P & q in P ) ; ::_thesis: Line (p,q) = P
reconsider Q = Line (p,q) as LINE of CLSP by A1, Def7;
 Q c= P by A1, A2, Th18;
hence  Line (p,q) = P by Th17; ::_thesis: verum
end;

theorem Th20: :: COLLSP:20
for CLSP being proper CollSp
for p, q being Point of CLSP
for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds
P = Q
proof
let CLSP be proper CollSp; ::_thesis: for p, q being Point of CLSP
for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds
P = Q
let p, q be Point of CLSP; ::_thesis: for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds
P = Q
let P, Q be LINE of CLSP; ::_thesis: ( p <> q & p in P & q in P & p in Q & q in Q implies P = Q )
assume that
A1: p <> q and
A2: ( p in P & q in P ) and
A3: ( p in Q & q in Q ) ; ::_thesis: P = Q
 Line (p,q) = P by A1, A2, Th19;
hence  P = Q by A1, A3, Th19; ::_thesis: verum
end;

theorem :: COLLSP:21
for CLSP being proper CollSp
for P, Q being LINE of CLSP holds
( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} )
proof
let CLSP be proper CollSp; ::_thesis: for P, Q being LINE of CLSP holds
( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} )
let P, Q be LINE of CLSP; ::_thesis: ( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} )
A1: ( ex a being set st {a} = P /\ Q implies ex p being Point of CLSP st P /\ Q = {p} )
proof
given a being set  such that A2: {a} = P /\ Q ; ::_thesis: ex p being Point of CLSP st P /\ Q = {p}
 a in P /\ Q by A2, TARSKI:def_1;
then  a in P by XBOOLE_0:def_4;
then reconsider p = a as Point of CLSP by Lm9;
 P /\ Q = {p} by A2;
hence  ex p being Point of CLSP st P /\ Q = {p} ; ::_thesis: verum
end;
A3: ( ex a, b being set st
( a <> b & a in P /\ Q & b in P /\ Q ) implies P = Q )
proof
given a, b being set  such that A4: a <> b and
A5: ( a in P /\ Q & b in P /\ Q ) ; ::_thesis: P = Q
 ( a in P & b in P ) by A5, XBOOLE_0:def_4;
then reconsider p = a, q = b as Point of CLSP by Lm9;
A6: ( p in Q & q in Q ) by A5, XBOOLE_0:def_4;
 ( p in P & q in P ) by A5, XBOOLE_0:def_4;
hence  P = Q by A4, A6, Th20; ::_thesis: verum
end;
 ( P /\ Q = {} or ex a being set st
( {a} = P /\ Q or ex a, b being set st
( a <> b & a in P /\ Q & b in P /\ Q ) ) ) by Th1;
hence  ( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} ) by A1, A3, XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: COLLSP:22
for CLSP being proper CollSp
for a, b being Point of CLSP st a <> b holds
Line (a,b) <> the carrier of CLSP
proof
let CLSP be proper CollSp; ::_thesis: for a, b being Point of CLSP st a <> b holds
Line (a,b) <> the carrier of CLSP
let a, b be Point of CLSP; ::_thesis: ( a <> b implies Line (a,b) <> the carrier of CLSP )
assume  a <> b ; ::_thesis: Line (a,b) <> the carrier of CLSP
then  not for r being Point of CLSP holds a,b,r is_collinear by Th12;
hence  Line (a,b) <> the carrier of CLSP by Th11; ::_thesis: verum
end;