:: COLLSP semantic presentation

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

:: deftheorem Def1 defines Relation3 COLLSP:def 1 :
for b1, b2 being set holds
( b2 is Relation3 of b1 iff b2 c= [:b1,b1,b1:] );

theorem Th1: :: COLLSP:1
canceled;

theorem Th2: :: COLLSP:2
for b1 being set holds
( b1 = {} or ex b2 being set st
( {b2} = b1 or ex b3, b4 being set st
( b3 <> b4 & b3 in b1 & b4 in b1 ) ) )
proof end;

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

registration
cluster non empty strict CollStr ;
existence
ex b1 being CollStr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let c1 be non empty CollStr ;
let c2, c3, c4 be Point of c1;
pred c2,c3,c4 is_collinear means :Def2: :: COLLSP:def 2
[a2,a3,a4] in the Collinearity of a1;
end;

:: deftheorem Def2 defines is_collinear COLLSP:def 2 :
for b1 being non empty CollStr
for b2, b3, b4 being Point of b1 holds
( b2,b3,b4 is_collinear iff [b2,b3,b4] in the Collinearity of b1 );

set c1 = {1};

Lemma4: 1 in {1}
by TARSKI:def 1;

Lemma5: {[1,1,1]} c= [:{1},{1},{1}:]
proof end;

reconsider c2 = {1} as non empty set by TARSKI:def 1;

reconsider c3 = {[1,1,1]} as Relation3 of c2 by Def1, Lemma5;

reconsider c4 = CollStr(# c2,c3 #) as non empty CollStr by STRUCT_0:def 1;

E6: now
E7: for b1, b2, b3 being Point of c4 holds [b1,b2,b3] in the Collinearity of c4
proof
let c5, c6, c7 be Point of c4;
( c5 = 1 & c6 = 1 & c7 = 1 ) by TARSKI:def 1;
hence [c5,c6,c7] in the Collinearity of c4 by TARSKI:def 1;
end;
let c5, c6, c7, c8, c9, c10 be Point of c4;
thus ( ( c5 = c6 or c5 = c7 or c6 = c7 ) implies [c5,c6,c7] in the Collinearity of c4 ) by E7;
thus ( c5 <> c6 & [c5,c6,c8] in the Collinearity of c4 & [c5,c6,c9] in the Collinearity of c4 & [c5,c6,c10] in the Collinearity of c4 implies [c8,c9,c10] in the Collinearity of c4 ) by E7;
end;

definition
let c5 be non empty CollStr ;
attr a1 is reflexive means :Def3: :: COLLSP:def 3
for b1, b2, b3 being Point of a1 st ( b1 = b2 or b1 = b3 or b2 = b3 ) holds
[b1,b2,b3] in the Collinearity of a1;
end;

:: deftheorem Def3 defines reflexive COLLSP:def 3 :
for b1 being non empty CollStr holds
( b1 is reflexive iff for b2, b3, b4 being Point of b1 st ( b2 = b3 or b2 = b4 or b3 = b4 ) holds
[b2,b3,b4] in the Collinearity of b1 );

definition
let c5 be non empty CollStr ;
attr a1 is transitive means :Def4: :: COLLSP:def 4
for b1, b2, b3, b4, b5 being Point of a1 st b1 <> b2 & [b1,b2,b3] in the Collinearity of a1 & [b1,b2,b4] in the Collinearity of a1 & [b1,b2,b5] in the Collinearity of a1 holds
[b3,b4,b5] in the Collinearity of a1;
end;

:: deftheorem Def4 defines transitive COLLSP:def 4 :
for b1 being non empty CollStr holds
( b1 is transitive iff for b2, b3, b4, b5, b6 being Point of b1 st b2 <> b3 & [b2,b3,b4] in the Collinearity of b1 & [b2,b3,b5] in the Collinearity of b1 & [b2,b3,b6] in the Collinearity of b1 holds
[b4,b5,b6] in the Collinearity of b1 );

registration
cluster non empty strict reflexive transitive CollStr ;
existence
ex b1 being non empty CollStr st
( b1 is strict & b1 is reflexive & b1 is transitive )
proof end;
end;

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

theorem Th3: :: COLLSP:3
canceled;

theorem Th4: :: COLLSP:4
canceled;

theorem Th5: :: COLLSP:5
canceled;

theorem Th6: :: COLLSP:6
canceled;

theorem Th7: :: COLLSP:7
for b1 being CollSp
for b2, b3, b4 being Point of b1 st ( b2 = b3 or b2 = b4 or b3 = b4 ) holds
b2,b3,b4 is_collinear
proof end;

theorem Th8: :: COLLSP:8
for b1 being CollSp
for b2, b3, b4, b5, b6 being Point of b1 st b2 <> b3 & b2,b3,b4 is_collinear & b2,b3,b5 is_collinear & b2,b3,b6 is_collinear holds
b4,b5,b6 is_collinear
proof end;

theorem Th9: :: COLLSP:9
for b1 being CollSp
for b2, b3, b4 being Point of b1 st b2,b3,b4 is_collinear holds
( b3,b2,b4 is_collinear & b2,b4,b3 is_collinear )
proof end;

theorem Th10: :: COLLSP:10
for b1 being CollSp
for b2, b3 being Point of b1 holds b2,b3,b2 is_collinear by Th7;

theorem Th11: :: COLLSP:11
for b1 being CollSp
for b2, b3, b4, b5 being Point of b1 st b2 <> b3 & b2,b3,b4 is_collinear & b2,b3,b5 is_collinear holds
b2,b4,b5 is_collinear
proof end;

theorem Th12: :: COLLSP:12
for b1 being CollSp
for b2, b3, b4 being Point of b1 st b2,b3,b4 is_collinear holds
b3,b2,b4 is_collinear by Th9;

theorem Th13: :: COLLSP:13
for b1 being CollSp
for b2, b3, b4 being Point of b1 st b2,b3,b4 is_collinear holds
b3,b4,b2 is_collinear
proof end;

theorem Th14: :: COLLSP:14
for b1 being CollSp
for b2, b3, b4, b5, b6 being Point of b1 st b2 <> b3 & b4,b5,b2 is_collinear & b4,b5,b3 is_collinear & b2,b3,b6 is_collinear holds
b4,b5,b6 is_collinear
proof end;

definition
let c5 be CollSp;
let c6, c7 be Point of c5;
func Line c2,c3 -> set equals :: COLLSP:def 5
{ b1 where B is Point of a1 : a2,a3,b1 is_collinear } ;
correctness
coherence
{ b1 where B is Point of c5 : c6,c7,b1 is_collinear } is set ;
;
end;

:: deftheorem Def5 defines Line COLLSP:def 5 :
for b1 being CollSp
for b2, b3 being Point of b1 holds Line b2,b3 = { b4 where B is Point of b1 : b2,b3,b4 is_collinear } ;

theorem Th15: :: COLLSP:15
canceled;

theorem Th16: :: COLLSP:16
for b1 being CollSp
for b2, b3 being Point of b1 holds
( b2 in Line b2,b3 & b3 in Line b2,b3 )
proof end;

theorem Th17: :: COLLSP:17
for b1 being CollSp
for b2, b3, b4 being Point of b1 holds
( b2,b3,b4 is_collinear iff b4 in Line b2,b3 )
proof end;

set c5 = {1,2,3};

set c6 = { [b1,b2,b3] where B is Nat, B is Nat, B is Nat : ( ( b1 = b2 or b2 = b3 or b3 = b1 ) & b1 in {1,2,3} & b2 in {1,2,3} & b3 in {1,2,3} ) } ;

Lemma17: { [b1,b2,b3] where B is Nat, B is Nat, B is Nat : ( ( b1 = b2 or b2 = b3 or b3 = b1 ) & b1 in {1,2,3} & b2 in {1,2,3} & b3 in {1,2,3} ) } c= [:{1,2,3},{1,2,3},{1,2,3}:]
proof end;

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

reconsider c8 = { [b1,b2,b3] where B is Nat, B is Nat, B is Nat : ( ( b1 = b2 or b2 = b3 or b3 = b1 ) & b1 in {1,2,3} & b2 in {1,2,3} & b3 in {1,2,3} ) } as Relation3 of c7 by Def1, Lemma17;

reconsider c9 = CollStr(# c7,c8 #) as non empty CollStr by STRUCT_0:def 1;

Lemma18: for b1, b2, b3 being Point of c9 holds
( [b1,b2,b3] in c8 iff ( ( b1 = b2 or b2 = b3 or b3 = b1 ) & b1 in c7 & b2 in c7 & b3 in c7 ) )
proof end;

Lemma19: for b1, b2, b3, b4, b5, b6 being Point of c9 st b1 <> b2 & [b1,b2,b4] in the Collinearity of c9 & [b1,b2,b5] in the Collinearity of c9 & [b1,b2,b6] in the Collinearity of c9 holds
[b4,b5,b6] in the Collinearity of c9
proof end;

Lemma20: not for b1, b2, b3 being Point of c9 holds b1,b2,b3 is_collinear
proof end;

Lemma21: c9 is CollSp
proof end;

definition
let c10 be non empty CollStr ;
attr a1 is proper means :Def6: :: COLLSP:def 6
not for b1, b2, b3 being Point of a1 holds b1,b2,b3 is_collinear ;
end;

:: deftheorem Def6 defines proper COLLSP:def 6 :
for b1 being non empty CollStr holds
( b1 is proper iff not for b2, b3, b4 being Point of b1 holds b2,b3,b4 is_collinear );

registration
cluster strict proper CollStr ;
existence
ex b1 being CollSp st
( b1 is strict & b1 is proper )
proof end;
end;

theorem Th18: :: COLLSP:18
canceled;

theorem Th19: :: COLLSP:19
for b1 being proper CollSp
for b2, b3 being Point of b1 st b2 <> b3 holds
ex b4 being Point of b1 st not b2,b3,b4 is_collinear
proof end;

definition
let c10 be proper CollSp;
mode LINE of c1 -> set means :Def7: :: COLLSP:def 7
ex b1, b2 being Point of a1 st
( b1 <> b2 & a2 = Line b1,b2 );
existence
ex b1 being set ex b2, b3 being Point of c10 st
( b2 <> b3 & b1 = Line b2,b3 )
proof end;
end;

:: deftheorem Def7 defines LINE COLLSP:def 7 :
for b1 being proper CollSp
for b2 being set holds
( b2 is LINE of b1 iff ex b3, b4 being Point of b1 st
( b3 <> b4 & b2 = Line b3,b4 ) );

theorem Th20: :: COLLSP:20
canceled;

theorem Th21: :: COLLSP:21
canceled;

theorem Th22: :: COLLSP:22
for b1 being proper CollSp
for b2, b3 being Point of b1 st b2 = b3 holds
Line b2,b3 = the carrier of b1
proof end;

theorem Th23: :: COLLSP:23
for b1 being proper CollSp
for b2 being LINE of b1 ex b3, b4 being Point of b1 st
( b3 <> b4 & b3 in b2 & b4 in b2 )
proof end;

theorem Th24: :: COLLSP:24
for b1 being proper CollSp
for b2, b3 being Point of b1 st b2 <> b3 holds
ex b4 being LINE of b1 st
( b2 in b4 & b3 in b4 )
proof end;

theorem Th25: :: COLLSP:25
for b1 being proper CollSp
for b2, b3, b4 being Point of b1
for b5 being LINE of b1 st b2 in b5 & b3 in b5 & b4 in b5 holds
b2,b3,b4 is_collinear
proof end;

Lemma26: for b1 being proper CollSp
for b2 being LINE of b1
for b3 being set st b3 in b2 holds
b3 is Point of b1
proof end;

theorem Th26: :: COLLSP:26
for b1 being proper CollSp
for b2, b3 being LINE of b1 st b2 c= b3 holds
b2 = b3
proof end;

theorem Th27: :: COLLSP:27
for b1 being proper CollSp
for b2, b3 being Point of b1
for b4 being LINE of b1 st b2 <> b3 & b2 in b4 & b3 in b4 holds
Line b2,b3 c= b4
proof end;

theorem Th28: :: COLLSP:28
for b1 being proper CollSp
for b2, b3 being Point of b1
for b4 being LINE of b1 st b2 <> b3 & b2 in b4 & b3 in b4 holds
Line b2,b3 = b4
proof end;

theorem Th29: :: COLLSP:29
for b1 being proper CollSp
for b2, b3 being Point of b1
for b4, b5 being LINE of b1 st b2 <> b3 & b2 in b4 & b3 in b4 & b2 in b5 & b3 in b5 holds
b4 = b5
proof end;

theorem Th30: :: COLLSP:30
for b1 being proper CollSp
for b2, b3 being LINE of b1 holds
( b2 = b3 or b2 misses b3 or ex b4 being Point of b1 st b2 /\ b3 = {b4} )
proof end;

theorem Th31: :: COLLSP:31
for b1 being proper CollSp
for b2, b3 being Point of b1 st b2 <> b3 holds
Line b2,b3 <> the carrier of b1
proof end;