:: PROJPL_1 semantic presentation

notation
let c1 be IncProjStr ;
let c2 be POINT of c1;
let c3 be LINE of c1;
antonym c2 |' c3 for c2 on c3;
end;

definition
let c1 be IncProjStr ;
let c2, c3 be POINT of c1;
let c4 be LINE of c1;
pred c2,c3 |' c4 means :Def1: :: PROJPL_1:def 1
( a2 |' a4 & a3 |' a4 );
end;

:: deftheorem Def1 defines |' PROJPL_1:def 1 :
for b1 being IncProjStr
for b2, b3 being POINT of b1
for b4 being LINE of b1 holds
( b2,b3 |' b4 iff ( b2 |' b4 & b3 |' b4 ) );

definition
let c1 be IncProjStr ;
let c2 be POINT of c1;
let c3, c4 be LINE of c1;
pred c2 on c3,c4 means :Def2: :: PROJPL_1:def 2
( a2 on a3 & a2 on a4 );
end;

:: deftheorem Def2 defines on PROJPL_1:def 2 :
for b1 being IncProjStr
for b2 being POINT of b1
for b3, b4 being LINE of b1 holds
( b2 on b3,b4 iff ( b2 on b3 & b2 on b4 ) );

definition
let c1 be IncProjStr ;
let c2 be POINT of c1;
let c3, c4, c5 be LINE of c1;
pred c2 on c3,c4,c5 means :Def3: :: PROJPL_1:def 3
( a2 on a3 & a2 on a4 & a2 on a5 );
end;

:: deftheorem Def3 defines on PROJPL_1:def 3 :
for b1 being IncProjStr
for b2 being POINT of b1
for b3, b4, b5 being LINE of b1 holds
( b2 on b3,b4,b5 iff ( b2 on b3 & b2 on b4 & b2 on b5 ) );

theorem Th1: :: PROJPL_1:1
for b1 being IncProjStr
for b2, b3, b4 being POINT of b1
for b5, b6, b7 being LINE of b1 holds
( ( b2,b3 on b5 implies b3,b2 on b5 ) & ( b2,b3,b4 on b5 implies ( b2,b4,b3 on b5 & b3,b2,b4 on b5 & b3,b4,b2 on b5 & b4,b2,b3 on b5 & b4,b3,b2 on b5 ) ) & ( b2 on b5,b6 implies b2 on b6,b5 ) & ( b2 on b5,b6,b7 implies ( b2 on b5,b7,b6 & b2 on b6,b5,b7 & b2 on b6,b7,b5 & b2 on b7,b5,b6 & b2 on b7,b6,b5 ) ) )
proof end;

definition
let c1 be IncProjStr ;
attr a1 is configuration means :Def4: :: PROJPL_1:def 4
for b1, b2 being POINT of a1
for b3, b4 being LINE of a1 st b1 on b3 & b2 on b3 & b1 on b4 & b2 on b4 & not b1 = b2 holds
b3 = b4;
end;

:: deftheorem Def4 defines configuration PROJPL_1:def 4 :
for b1 being IncProjStr holds
( b1 is configuration iff for b2, b3 being POINT of b1
for b4, b5 being LINE of b1 st b2 on b4 & b3 on b4 & b2 on b5 & b3 on b5 & not b2 = b3 holds
b4 = b5 );

theorem Th2: :: PROJPL_1:2
for b1 being IncProjStr holds
( b1 is configuration iff for b2, b3 being POINT of b1
for b4, b5 being LINE of b1 st b2,b3 on b4 & b2,b3 on b5 & not b2 = b3 holds
b4 = b5 )
proof end;

theorem Th3: :: PROJPL_1:3
for b1 being IncProjStr holds
( b1 is configuration iff for b2, b3 being POINT of b1
for b4, b5 being LINE of b1 st b2 on b4,b5 & b3 on b4,b5 & not b2 = b3 holds
b4 = b5 )
proof end;

theorem Th4: :: PROJPL_1:4
for b1 being IncProjStr holds
( b1 is IncProjSp iff ( b1 is configuration & ( for b2, b3 being POINT of b1 ex b4 being LINE of b1 st b2,b3 on b4 ) & ex b2 being POINT of b1ex b3 being LINE of b1 st b2 |' b3 & ( for b2 being LINE of b1 ex b3, b4, b5 being POINT of b1 st
( b3,b4,b5 are_mutually_different & b3,b4,b5 on b2 ) ) & ( for b2, b3, b4, b5, b6 being POINT of b1
for b7, b8, b9, b10 being LINE of b1 st b2,b3,b6 on b7 & b4,b5,b6 on b8 & b2,b4 on b9 & b3,b5 on b10 & b6 |' b9 & b6 |' b10 & b7 <> b8 holds
ex b11 being POINT of b1 st b11 on b9,b10 ) ) )
proof end;

definition
mode IncProjectivePlane is 2-dimensional IncProjSp;
end;

definition
let c1 be IncProjStr ;
let c2, c3, c4 be POINT of c1;
pred c2,c3,c4 is_collinear means :Def5: :: PROJPL_1:def 5
ex b1 being LINE of a1 st a2,a3,a4 on b1;
end;

:: deftheorem Def5 defines is_collinear PROJPL_1:def 5 :
for b1 being IncProjStr
for b2, b3, b4 being POINT of b1 holds
( b2,b3,b4 is_collinear iff ex b5 being LINE of b1 st b2,b3,b4 on b5 );

notation
let c1 be IncProjStr ;
let c2, c3, c4 be POINT of c1;
antonym c2,c3,c4 is_a_triangle for c2,c3,c4 is_collinear ;
end;

theorem Th5: :: PROJPL_1:5
for b1 being IncProjStr
for b2, b3, b4 being POINT of b1 holds
( b2,b3,b4 is_collinear iff ex b5 being LINE of b1 st
( b2 on b5 & b3 on b5 & b4 on b5 ) )
proof end;

theorem Th6: :: PROJPL_1:6
for b1 being IncProjStr
for b2, b3, b4 being POINT of b1 holds
( b2,b3,b4 is_a_triangle iff for b5 being LINE of b1 holds
( b2 |' b5 or b3 |' b5 or b4 |' b5 ) ) by Th5;

definition
let c1 be IncProjStr ;
let c2, c3, c4, c5 be POINT of c1;
pred c2,c3,c4,c5 is_a_quadrangle means :Def6: :: PROJPL_1:def 6
( a2,a3,a4 is_a_triangle & a3,a4,a5 is_a_triangle & a4,a5,a2 is_a_triangle & a5,a2,a3 is_a_triangle );
end;

:: deftheorem Def6 defines is_a_quadrangle PROJPL_1:def 6 :
for b1 being IncProjStr
for b2, b3, b4, b5 being POINT of b1 holds
( b2,b3,b4,b5 is_a_quadrangle iff ( b2,b3,b4 is_a_triangle & b3,b4,b5 is_a_triangle & b4,b5,b2 is_a_triangle & b5,b2,b3 is_a_triangle ) );

theorem Th7: :: PROJPL_1:7
for b1 being IncProjStr st b1 is IncProjSp holds
ex b2, b3 being LINE of b1 st b2 <> b3
proof end;

theorem Th8: :: PROJPL_1:8
for b1 being IncProjStr
for b2 being POINT of b1
for b3 being LINE of b1 st b1 is IncProjSp & b2 on b3 holds
ex b4, b5 being POINT of b1 st
( b4,b5 on b3 & b2,b4,b5 are_mutually_different )
proof end;

theorem Th9: :: PROJPL_1:9
for b1 being IncProjStr
for b2 being POINT of b1
for b3, b4 being LINE of b1 st b1 is IncProjSp & b2 on b3 & b3 <> b4 holds
ex b5 being POINT of b1 st
( b5 on b3 & b5 |' b4 & b2 <> b5 )
proof end;

theorem Th10: :: PROJPL_1:10
for b1 being IncProjStr
for b2, b3, b4 being POINT of b1
for b5 being LINE of b1 st b1 is configuration & b2,b3 on b5 & b2 <> b3 & b4 |' b5 holds
b2,b3,b4 is_a_triangle
proof end;

theorem Th11: :: PROJPL_1:11
for b1 being IncProjStr
for b2, b3, b4 being POINT of b1 st b2,b3,b4 is_collinear holds
( b2,b4,b3 is_collinear & b3,b2,b4 is_collinear & b3,b4,b2 is_collinear & b4,b2,b3 is_collinear & b4,b3,b2 is_collinear )
proof end;

theorem Th12: :: PROJPL_1:12
for b1 being IncProjStr
for b2, b3, b4 being POINT of b1 st b2,b3,b4 is_a_triangle holds
( b2,b4,b3 is_a_triangle & b3,b2,b4 is_a_triangle & b3,b4,b2 is_a_triangle & b4,b2,b3 is_a_triangle & b4,b3,b2 is_a_triangle ) by Th11;

theorem Th13: :: PROJPL_1:13
for b1 being IncProjStr
for b2, b3, b4, b5 being POINT of b1 st b2,b3,b4,b5 is_a_quadrangle holds
( b2,b4,b3,b5 is_a_quadrangle & b3,b2,b4,b5 is_a_quadrangle & b3,b4,b2,b5 is_a_quadrangle & b4,b2,b3,b5 is_a_quadrangle & b4,b3,b2,b5 is_a_quadrangle & b2,b3,b5,b4 is_a_quadrangle & b2,b4,b5,b3 is_a_quadrangle & b3,b2,b5,b4 is_a_quadrangle & b3,b4,b5,b2 is_a_quadrangle & b4,b2,b5,b3 is_a_quadrangle & b4,b3,b5,b2 is_a_quadrangle & b2,b5,b3,b4 is_a_quadrangle & b2,b5,b4,b3 is_a_quadrangle & b3,b5,b2,b4 is_a_quadrangle & b3,b5,b4,b2 is_a_quadrangle & b4,b5,b2,b3 is_a_quadrangle & b4,b5,b3,b2 is_a_quadrangle & b5,b2,b3,b4 is_a_quadrangle & b5,b2,b4,b3 is_a_quadrangle & b5,b3,b2,b4 is_a_quadrangle & b5,b3,b4,b2 is_a_quadrangle & b5,b4,b2,b3 is_a_quadrangle & b5,b4,b3,b2 is_a_quadrangle )
proof end;

theorem Th14: :: PROJPL_1:14
for b1 being IncProjStr
for b2, b3, b4, b5 being POINT of b1
for b6, b7 being LINE of b1 st b1 is configuration & b2,b3 on b6 & b4,b5 on b7 & b2,b3 |' b7 & b4,b5 |' b6 & b2 <> b3 & b4 <> b5 holds
b2,b3,b4,b5 is_a_quadrangle
proof end;

theorem Th15: :: PROJPL_1:15
for b1 being IncProjStr st b1 is IncProjSp holds
ex b2, b3, b4, b5 being POINT of b1 st b2,b3,b4,b5 is_a_quadrangle
proof end;

definition
let c1 be IncProjSp;
mode Quadrangle of c1 -> Element of [:the Points of a1,the Points of a1,the Points of a1,the Points of a1:] means :: PROJPL_1:def 7
a2 `1 ,a2 `2 ,a2 `3 ,a2 `4 is_a_quadrangle ;
existence
ex b1 being Element of [:the Points of c1,the Points of c1,the Points of c1,the Points of c1:] st b1 `1 ,b1 `2 ,b1 `3 ,b1 `4 is_a_quadrangle
proof end;
end;

:: deftheorem Def7 defines Quadrangle PROJPL_1:def 7 :
for b1 being IncProjSp
for b2 being Element of [:the Points of b1,the Points of b1,the Points of b1,the Points of b1:] holds
( b2 is Quadrangle of b1 iff b2 `1 ,b2 `2 ,b2 `3 ,b2 `4 is_a_quadrangle );

definition
let c1 be IncProjSp;
let c2, c3 be POINT of c1;
assume E20: c2 <> c3 ;
func c2 * c3 -> LINE of a1 means :Def8: :: PROJPL_1:def 8
a2,a3 on a4;
existence
ex b1 being LINE of c1 st c2,c3 on b1 by Th4;
uniqueness
for b1, b2 being LINE of c1 st c2,c3 on b1 & c2,c3 on b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines * PROJPL_1:def 8 :
for b1 being IncProjSp
for b2, b3 being POINT of b1 st b2 <> b3 holds
for b4 being LINE of b1 holds
( b4 = b2 * b3 iff b2,b3 on b4 );

theorem Th16: :: PROJPL_1:16
for b1 being IncProjSp
for b2, b3 being POINT of b1
for b4 being LINE of b1 st b2 <> b3 holds
( b2 on b2 * b3 & b3 on b2 * b3 & b2 * b3 = b3 * b2 & ( b2 on b4 & b3 on b4 implies b4 = b2 * b3 ) )
proof end;

theorem Th17: :: PROJPL_1:17
for b1 being IncProjStr st ex b2, b3, b4 being POINT of b1 st b2,b3,b4 is_a_triangle & ( for b2, b3 being POINT of b1 ex b4 being LINE of b1 st b2,b3 on b4 ) holds
ex b2 being POINT of b1ex b3 being LINE of b1 st b2 |' b3
proof end;

theorem Th18: :: PROJPL_1:18
for b1 being IncProjStr st ex b2, b3, b4, b5 being POINT of b1 st b2,b3,b4,b5 is_a_quadrangle holds
ex b2, b3, b4 being POINT of b1 st b2,b3,b4 is_a_triangle
proof end;

theorem Th19: :: PROJPL_1:19
for b1 being IncProjStr
for b2, b3, b4 being POINT of b1
for b5, b6 being LINE of b1 st b2,b3,b4 is_a_triangle & b2,b3 on b5 & b2,b4 on b6 holds
b5 <> b6
proof end;

theorem Th20: :: PROJPL_1:20
for b1 being IncProjStr
for b2, b3, b4, b5 being POINT of b1
for b6, b7, b8 being LINE of b1 st b2,b3,b4,b5 is_a_quadrangle & b2,b3 on b6 & b2,b4 on b7 & b2,b5 on b8 holds
b6,b7,b8 are_mutually_different
proof end;

theorem Th21: :: PROJPL_1:21
for b1 being IncProjStr
for b2, b3, b4, b5 being POINT of b1
for b6, b7, b8, b9 being LINE of b1 st b1 is configuration & b2 on b6,b7,b8 & b6,b7,b8 are_mutually_different & b2 |' b9 & b3 on b9,b6 & b4 on b9,b7 & b5 on b9,b8 holds
b3,b4,b5 are_mutually_different
proof end;

theorem Th22: :: PROJPL_1:22
for b1 being IncProjStr st b1 is configuration & ( for b2, b3 being POINT of b1 ex b4 being LINE of b1 st b2,b3 on b4 ) & ( for b2, b3 being LINE of b1 ex b4 being POINT of b1 st b4 on b2,b3 ) & ex b2, b3, b4, b5 being POINT of b1 st b2,b3,b4,b5 is_a_quadrangle holds
for b2 being LINE of b1 ex b3, b4, b5 being POINT of b1 st
( b3,b4,b5 are_mutually_different & b3,b4,b5 on b2 )
proof end;

theorem Th23: :: PROJPL_1:23
for b1 being IncProjStr holds
( b1 is IncProjectivePlane iff ( b1 is configuration & ( for b2, b3 being POINT of b1 ex b4 being LINE of b1 st b2,b3 on b4 ) & ( for b2, b3 being LINE of b1 ex b4 being POINT of b1 st b4 on b2,b3 ) & ex b2, b3, b4, b5 being POINT of b1 st b2,b3,b4,b5 is_a_quadrangle ) )
proof end;

definition
let c1 be IncProjectivePlane;
let c2, c3 be LINE of c1;
assume E29: c2 <> c3 ;
func c2 * c3 -> POINT of a1 means :Def9: :: PROJPL_1:def 9
a4 on a2,a3;
existence
ex b1 being POINT of c1 st b1 on c2,c3 by Th23;
uniqueness
for b1, b2 being POINT of c1 st b1 on c2,c3 & b2 on c2,c3 holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines * PROJPL_1:def 9 :
for b1 being IncProjectivePlane
for b2, b3 being LINE of b1 st b2 <> b3 holds
for b4 being POINT of b1 holds
( b4 = b2 * b3 iff b4 on b2,b3 );

theorem Th24: :: PROJPL_1:24
for b1 being IncProjectivePlane
for b2 being POINT of b1
for b3, b4 being LINE of b1 st b3 <> b4 holds
( b3 * b4 on b3 & b3 * b4 on b4 & b3 * b4 = b4 * b3 & ( b2 on b3 & b2 on b4 implies b2 = b3 * b4 ) )
proof end;

theorem Th25: :: PROJPL_1:25
for b1 being IncProjectivePlane
for b2, b3 being POINT of b1
for b4, b5 being LINE of b1 st b4 <> b5 & b2 on b4 & b3 |' b4 & b2 <> b4 * b5 holds
( (b3 * b2) * b5 on b5 & (b3 * b2) * b5 |' b4 )
proof end;

theorem Th26: :: PROJPL_1:26
for b1 being IncProjSp
for b2, b3, b4 being POINT of b1 st b2,b3,b4 is_a_triangle holds
b2,b3,b4 are_mutually_different
proof end;

theorem Th27: :: PROJPL_1:27
for b1 being IncProjSp
for b2, b3, b4, b5 being POINT of b1 st b2,b3,b4,b5 is_a_quadrangle holds
b2,b3,b4,b5 are_mutually_different
proof end;

theorem Th28: :: PROJPL_1:28
for b1 being IncProjectivePlane
for b2, b3, b4, b5 being POINT of b1 holds
( not b2 * b4 = b3 * b5 or b2 = b4 or b3 = b5 or b4 = b5 or b2 * b4 = b4 * b5 )
proof end;

theorem Th29: :: PROJPL_1:29
for b1 being IncProjectivePlane
for b2, b3, b4, b5 being POINT of b1 holds
( not b2 * b4 = b3 * b5 or b2 = b4 or b3 = b5 or b4 = b5 or b2 on b4 * b5 )
proof end;

theorem Th30: :: PROJPL_1:30
for b1 being IncProjectivePlane
for b2, b3, b4 being POINT of b1
for b5 being LINE of b1 st b3 on b5 & b4 on b5 & b3 <> b4 & b2 |' b5 holds
( b3 * b2 <> b4 * b2 & b2 * b3 <> b2 * b4 )
proof end;

theorem Th31: :: PROJPL_1:31
for b1 being IncProjectivePlane
for b2 being POINT of b1
for b3, b4, b5 being LINE of b1 st b2 on b4 & b2 on b5 & b4 <> b5 & b2 |' b3 holds
( b3 * b4 <> b3 * b5 & b4 * b3 <> b5 * b3 )
proof end;

theorem Th32: :: PROJPL_1:32
for b1 being IncProjSp
for b2, b3, b4, b5 being POINT of b1 st b4 on b2 * b3 & b4 on b2 * b5 & b4 <> b2 & b5 <> b2 & b2 <> b3 holds
b5 on b2 * b3
proof end;

theorem Th33: :: PROJPL_1:33
for b1 being IncProjSp
for b2, b3, b4 being POINT of b1 st b4 on b2 * b3 & b2 <> b4 holds
b3 on b2 * b4
proof end;

theorem Th34: :: PROJPL_1:34
for b1 being IncProjectivePlane
for b2, b3, b4, b5 being POINT of b1
for b6 being LINE of b1 st b4 <> b5 & b4 on b6 & b5 on b6 & b2 |' b6 & b3 |' b6 holds
b2 * b4 <> b3 * b5
proof end;

theorem Th35: :: PROJPL_1:35
for b1 being IncProjectivePlane
for b2, b3, b4 being POINT of b1 holds
( not b2 on b3 * b4 or b2 = b4 or b3 = b4 or b3 on b4 * b2 )
proof end;

theorem Th36: :: PROJPL_1:36
for b1 being IncProjectivePlane
for b2, b3, b4 being POINT of b1 holds
( not b2 on b3 * b4 or b3 = b2 or b3 = b4 or b4 on b3 * b2 )
proof end;

theorem Th37: :: PROJPL_1:37
for b1 being IncProjectivePlane
for b2, b3, b4, b5, b6 being POINT of b1
for b7, b8 being LINE of b1 st b3 on b8 & b4 on b8 & b2 on b7 & b2 |' b8 & b3 <> b4 & b5 <> b2 & b6 <> b2 & b5 on b2 * b3 & b6 on b2 * b4 holds
ex b9 being POINT of b1 st
( b9 on b5 * b6 & b9 on b7 & b9 <> b2 )
proof end;