:: INCPROJ semantic presentation

definition
let c1 be proper CollSp;
redefine mode LINE as LINE of c1 -> Subset of a1;
coherence
for b1 being LINE of c1 holds b1 is Subset of c1
proof end;
end;

definition
let c1 be proper CollSp;
func ProjectiveLines c1 -> set equals :: INCPROJ:def 1
{ b1 where B is Subset of a1 : b1 is LINE of a1 } ;
coherence
{ b1 where B is Subset of c1 : b1 is LINE of c1 } is set ;
end;

:: deftheorem Def1 defines ProjectiveLines INCPROJ:def 1 :
for b1 being proper CollSp holds ProjectiveLines b1 = { b2 where B is Subset of b1 : b2 is LINE of b1 } ;

registration
let c1 be proper CollSp;
cluster ProjectiveLines a1 -> non empty ;
coherence
not ProjectiveLines c1 is empty
proof end;
end;

theorem Th1: :: INCPROJ:1
canceled;

theorem Th2: :: INCPROJ:2
for b1 being proper CollSp
for b2 being set holds
( b2 is LINE of b1 iff b2 is Element of ProjectiveLines b1 )
proof end;

definition
let c1 be proper CollSp;
func Proj_Inc c1 -> Relation of the carrier of a1, ProjectiveLines a1 means :Def2: :: INCPROJ:def 2
for b1, b2 being set holds
( [b1,b2] in a2 iff ( b1 in the carrier of a1 & b2 in ProjectiveLines a1 & ex b3 being set st
( b2 = b3 & b1 in b3 ) ) );
existence
ex b1 being Relation of the carrier of c1, ProjectiveLines c1 st
for b2, b3 being set holds
( [b2,b3] in b1 iff ( b2 in the carrier of c1 & b3 in ProjectiveLines c1 & ex b4 being set st
( b3 = b4 & b2 in b4 ) ) )
proof end;
uniqueness
for b1, b2 being Relation of the carrier of c1, ProjectiveLines c1 st ( for b3, b4 being set holds
( [b3,b4] in b1 iff ( b3 in the carrier of c1 & b4 in ProjectiveLines c1 & ex b5 being set st
( b4 = b5 & b3 in b5 ) ) ) ) & ( for b3, b4 being set holds
( [b3,b4] in b2 iff ( b3 in the carrier of c1 & b4 in ProjectiveLines c1 & ex b5 being set st
( b4 = b5 & b3 in b5 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Proj_Inc INCPROJ:def 2 :
for b1 being proper CollSp
for b2 being Relation of the carrier of b1, ProjectiveLines b1 holds
( b2 = Proj_Inc b1 iff for b3, b4 being set holds
( [b3,b4] in b2 iff ( b3 in the carrier of b1 & b4 in ProjectiveLines b1 & ex b5 being set st
( b4 = b5 & b3 in b5 ) ) ) );

definition
let c1 be proper CollSp;
func IncProjSp_of c1 -> IncProjStr equals :: INCPROJ:def 3
 IncProjStr(# the carrier of a1,(ProjectiveLines a1),(Proj_Inc a1) #);
coherence
IncProjStr(# the carrier of c1,(ProjectiveLines c1),(Proj_Inc c1) #) is IncProjStr ;
end;

:: deftheorem Def3 defines IncProjSp_of INCPROJ:def 3 :
for b1 being proper CollSp holds IncProjSp_of b1 = IncProjStr(# the carrier of b1,(ProjectiveLines b1),(Proj_Inc b1) #);

registration
let c1 be proper CollSp;
cluster IncProjSp_of a1 -> strict ;
coherence
IncProjSp_of c1 is strict ;
end;

theorem Th3: :: INCPROJ:3
canceled;

theorem Th4: :: INCPROJ:4
for b1 being proper CollSp holds
( the Points of (IncProjSp_of b1) = the carrier of b1 & the Lines of (IncProjSp_of b1) = ProjectiveLines b1 & the Inc of (IncProjSp_of b1) = Proj_Inc b1 ) ;

theorem Th5: :: INCPROJ:5
for b1 being proper CollSp
for b2 being set holds
( b2 is Point of b1 iff b2 is POINT of (IncProjSp_of b1) ) ;

theorem Th6: :: INCPROJ:6
for b1 being proper CollSp
for b2 being set holds
( b2 is LINE of b1 iff b2 is LINE of (IncProjSp_of b1) ) by Th2;

theorem Th7: :: INCPROJ:7
canceled;

theorem Th8: :: INCPROJ:8
for b1 being proper CollSp
for b2 being POINT of (IncProjSp_of b1)
for b3 being LINE of (IncProjSp_of b1) holds
( b2 on b3 iff [b2,b3] in Proj_Inc b1 ) by INCSP_1:def 1;

theorem Th9: :: INCPROJ:9
for b1 being proper CollSp
for b2 being POINT of (IncProjSp_of b1)
for b3 being LINE of (IncProjSp_of b1)
for b4 being Point of b1
for b5 being LINE of b1 st b2 = b4 & b3 = b5 holds
( b2 on b3 iff b4 in b5 )
proof end;

theorem Th10: :: INCPROJ:10
for b1 being proper CollSp ex b2, b3, b4 being Point of b1 st
( b2 <> b3 & b3 <> b4 & b4 <> b2 )
proof end;

theorem Th11: :: INCPROJ:11
for b1 being proper CollSp
for b2 being Point of b1 ex b3 being Point of b1 st b2 <> b3
proof end;

theorem Th12: :: INCPROJ:12
for b1 being proper CollSp
for b2, b3 being POINT of (IncProjSp_of b1)
for b4, b5 being LINE of (IncProjSp_of b1) st b2 on b4 & b3 on b4 & b2 on b5 & b3 on b5 & not b2 = b3 holds
b4 = b5
proof end;

theorem Th13: :: INCPROJ:13
for b1 being proper CollSp
for b2, b3 being POINT of (IncProjSp_of b1) ex b4 being LINE of (IncProjSp_of b1) st
( b2 on b4 & b3 on b4 )
proof end;

theorem Th14: :: INCPROJ:14
for b1 being proper CollSp
for b2, b3, b4 being POINT of (IncProjSp_of b1)
for b5, b6, b7 being Point of b1 st b2 = b5 & b3 = b6 & b4 = b7 holds
( b5,b6,b7 is_collinear iff ex b8 being LINE of (IncProjSp_of b1) st
( b2 on b8 & b3 on b8 & b4 on b8 ) )
proof end;

theorem Th15: :: INCPROJ:15
for b1 being proper CollSp holds
not for b2 being POINT of (IncProjSp_of b1)
for b3 being LINE of (IncProjSp_of b1) holds b2 on b3
proof end;

theorem Th16: :: INCPROJ:16
for b1 being CollProjectiveSpace
for b2 being LINE of (IncProjSp_of b1) ex b3, b4, b5 being POINT of (IncProjSp_of b1) st
( b3 <> b4 & b4 <> b5 & b5 <> b3 & b3 on b2 & b4 on b2 & b5 on b2 )
proof end;

theorem Th17: :: INCPROJ:17
for b1 being CollProjectiveSpace
for b2, b3, b4, b5, b6 being POINT of (IncProjSp_of b1)
for b7, b8, b9, b10 being LINE of (IncProjSp_of b1) st b2 on b7 & b3 on b7 & b4 on b8 & b5 on b8 & b6 on b7 & b6 on b8 & b2 on b9 & b4 on b9 & b3 on b10 & b5 on b10 & not b6 on b9 & not b6 on b10 & b7 <> b8 holds
ex b11 being POINT of (IncProjSp_of b1) st
( b11 on b9 & b11 on b10 )
proof end;

theorem Th18: :: INCPROJ:18
for b1 being CollProjectiveSpace st ( for b2, b3, b4, b5 being Point of b1 ex b6 being Point of b1 st
( b2,b3,b6 is_collinear & b4,b5,b6 is_collinear ) ) holds
for b2, b3 being LINE of (IncProjSp_of b1) ex b4 being POINT of (IncProjSp_of b1) st
( b4 on b2 & b4 on b3 )
proof end;

theorem Th19: :: INCPROJ:19
for b1 being CollProjectiveSpace st ex b2, b3, b4, b5 being Point of b1 st
for b6 being Point of b1 holds
( not b2,b3,b6 is_collinear or not b4,b5,b6 is_collinear ) holds
ex b2, b3 being LINE of (IncProjSp_of b1) st
for b4 being POINT of (IncProjSp_of b1) holds
( not b4 on b2 or not b4 on b3 )
proof end;

theorem Th20: :: INCPROJ:20
for b1 being CollProjectiveSpace st ( for b2, b3, b4, b5, b6 being Point of b1 ex b7, b8 being Point of b1 st
( b2,b4,b7 is_collinear & b3,b5,b8 is_collinear & b6,b7,b8 is_collinear ) ) holds
for b2 being POINT of (IncProjSp_of b1)
for b3, b4 being LINE of (IncProjSp_of b1) ex b5, b6 being POINT of (IncProjSp_of b1)ex b7 being LINE of (IncProjSp_of b1) st
( b2 on b7 & b5 on b7 & b6 on b7 & b5 on b3 & b6 on b4 )
proof end;

definition
let c1, c2, c3 be set ;
canceled;
pred c1,c2,c3 are_mutually_different means :Def5: :: INCPROJ:def 5
( a1 <> a2 & a2 <> a3 & a3 <> a1 );
let c4 be set ;
pred c1,c2,c3,c4 are_mutually_different means :Def6: :: INCPROJ:def 6
( a1 <> a2 & a2 <> a3 & a3 <> a1 & a4 <> a1 & a4 <> a2 & a4 <> a3 );
end;

:: deftheorem Def4 INCPROJ:def 4 :
canceled;

:: deftheorem Def5 defines are_mutually_different INCPROJ:def 5 :
for b1, b2, b3 being set holds
( b1,b2,b3 are_mutually_different iff ( b1 <> b2 & b2 <> b3 & b3 <> b1 ) );

:: deftheorem Def6 defines are_mutually_different INCPROJ:def 6 :
for b1, b2, b3, b4 being set holds
( b1,b2,b3,b4 are_mutually_different iff ( b1 <> b2 & b2 <> b3 & b3 <> b1 & b4 <> b1 & b4 <> b2 & b4 <> b3 ) );

definition
let c1 be IncProjStr ;
let c2, c3 be POINT of c1;
let c4 be LINE of c1;
pred c2,c3 on c4 means :Def7: :: INCPROJ:def 7
( a2 on a4 & a3 on a4 );
let c5 be POINT of c1;
pred c2,c3,c5 on c4 means :Def8: :: INCPROJ:def 8
( a2 on a4 & a3 on a4 & a5 on a4 );
end;

:: deftheorem Def7 defines on INCPROJ:def 7 :
for b1 being IncProjStr
for b2, b3 being POINT of b1
for b4 being LINE of b1 holds
( b2,b3 on b4 iff ( b2 on b4 & b3 on b4 ) );

:: deftheorem Def8 defines on INCPROJ:def 8 :
for b1 being IncProjStr
for b2, b3 being POINT of b1
for b4 being LINE of b1
for b5 being POINT of b1 holds
( b2,b3,b5 on b4 iff ( b2 on b4 & b3 on b4 & b5 on b4 ) );

theorem Th21: :: INCPROJ:21
for b1 being CollProjectiveSpace st ( for b2, b3, b4, b5, b6, b7, b8 being Point of b1 st b2,b3,b4 is_collinear & b5,b6,b4 is_collinear & b2,b5,b7 is_collinear & b3,b6,b7 is_collinear & b2,b6,b8 is_collinear & b3,b5,b8 is_collinear & b7,b4,b8 is_collinear & not b2,b3,b6 is_collinear & not b2,b3,b5 is_collinear & not b2,b5,b6 is_collinear holds
b3,b5,b6 is_collinear ) holds
for b2, b3, b4, b5, b6, b7, b8 being POINT of (IncProjSp_of b1)
for b9, b10, b11, b12, b13, b14, b15 being LINE of (IncProjSp_of b1) st not b3 on b9 & not b4 on b9 & not b2 on b10 & not b5 on b10 & not b2 on b11 & not b4 on b11 & not b3 on b12 & not b5 on b12 & b6,b2,b5 on b9 & b6,b3,b4 on b10 & b7,b3,b5 on b11 & b7,b2,b4 on b12 & b8,b2,b3 on b13 & b8,b4,b5 on b14 & b6,b7 on b15 holds
not b8 on b15
proof end;

theorem Th22: :: INCPROJ:22
for b1 being CollProjectiveSpace st ( for b2, b3, b4, b5, b6, b7, b8, b9, b10, b11 being Point of b1 st b2 <> b6 & b3 <> b6 & b2 <> b7 & b4 <> b7 & b2 <> b8 & b5 <> b8 & not b2,b3,b4 is_collinear & not b2,b3,b5 is_collinear & not b2,b4,b5 is_collinear & b3,b4,b11 is_collinear & b6,b7,b11 is_collinear & b4,b5,b9 is_collinear & b7,b8,b9 is_collinear & b3,b5,b10 is_collinear & b6,b8,b10 is_collinear & b2,b3,b6 is_collinear & b2,b4,b7 is_collinear & b2,b5,b8 is_collinear holds
b9,b10,b11 is_collinear ) holds
for b2, b3, b4, b5, b6, b7, b8, b9, b10, b11 being POINT of (IncProjSp_of b1)
for b12, b13, b14, b15, b16, b17, b18, b19, b20 being LINE of (IncProjSp_of b1) st b2,b3,b4 on b12 & b2,b6,b5 on b13 & b2,b8,b7 on b14 & b8,b6,b11 on b15 & b8,b9,b4 on b16 & b6,b10,b4 on b17 & b11,b5,b7 on b18 & b3,b9,b7 on b19 & b3,b10,b5 on b20 & b12,b13,b14 are_mutually_different & b2 <> b4 & b2 <> b6 & b2 <> b8 & b2 <> b3 & b2 <> b5 & b2 <> b7 & b4 <> b3 & b6 <> b5 & b8 <> b7 holds
ex b21 being LINE of (IncProjSp_of b1) st b9,b10,b11 on b21
proof end;

theorem Th23: :: INCPROJ:23
for b1 being CollProjectiveSpace st ( for b2, b3, b4, b5, b6, b7, b8, b9, b10, b11 being Point of b1 st b2 <> b4 & b2 <> b5 & b4 <> b5 & b3 <> b4 & b3 <> b5 & b2 <> b7 & b2 <> b8 & b7 <> b8 & b6 <> b7 & b6 <> b8 & not b2,b3,b6 is_collinear & b2,b3,b4 is_collinear & b2,b3,b5 is_collinear & b2,b6,b7 is_collinear & b2,b6,b8 is_collinear & b3,b7,b11 is_collinear & b6,b4,b11 is_collinear & b3,b8,b10 is_collinear & b5,b6,b10 is_collinear & b4,b8,b9 is_collinear & b5,b7,b9 is_collinear holds
b9,b10,b11 is_collinear ) holds
for b2, b3, b4, b5, b6, b7, b8, b9, b10, b11 being POINT of (IncProjSp_of b1)
for b12, b13, b14, b15, b16, b17, b18, b19, b20 being LINE of (IncProjSp_of b1) st b2,b3,b4,b5 are_mutually_different & b2,b6,b7,b8 are_mutually_different & b14 <> b17 & b2 on b14 & b2 on b17 & b4,b8,b9 on b12 & b5,b6,b10 on b15 & b3,b7,b11 on b18 & b3,b8,b10 on b13 & b5,b7,b9 on b16 & b4,b6,b11 on b19 & b6,b7,b8 on b14 & b3,b4,b5 on b17 & b9,b10 on b20 holds
b11 on b20
proof end;

definition
let c1 be IncProjStr ;
attr a1 is partial means :Def9: :: INCPROJ:def 9
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;
attr a1 is linear means :Def10: :: INCPROJ:def 10
for b1, b2 being POINT of a1 ex b3 being LINE of a1 st
( b1 on b3 & b2 on b3 );
attr a1 is up-2-dimensional means :Def11: :: INCPROJ:def 11
not for b1 being POINT of a1
for b2 being LINE of a1 holds b1 on b2;
attr a1 is up-3-rank means :Def12: :: INCPROJ:def 12
for b1 being LINE of a1 ex b2, b3, b4 being POINT of a1 st
( b2 <> b3 & b3 <> b4 & b4 <> b2 & b2 on b1 & b3 on b1 & b4 on b1 );
attr a1 is Vebleian means :Def13: :: INCPROJ:def 13
for b1, b2, b3, b4, b5, b6 being POINT of a1
for b7, b8, b9, b10 being LINE of a1 st b1 on b7 & b2 on b7 & b3 on b8 & b4 on b8 & b5 on b7 & b5 on b8 & b1 on b9 & b3 on b9 & b2 on b10 & b4 on b10 & not b5 on b9 & not b5 on b10 & b7 <> b8 holds
ex b11 being POINT of a1 st
( b11 on b9 & b11 on b10 );
end;

:: deftheorem Def9 defines partial INCPROJ:def 9 :
for b1 being IncProjStr holds
( b1 is partial 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 );

:: deftheorem Def10 defines linear INCPROJ:def 10 :
for b1 being IncProjStr holds
( b1 is linear iff for b2, b3 being POINT of b1 ex b4 being LINE of b1 st
( b2 on b4 & b3 on b4 ) );

:: deftheorem Def11 defines up-2-dimensional INCPROJ:def 11 :
for b1 being IncProjStr holds
( b1 is up-2-dimensional iff not for b2 being POINT of b1
for b3 being LINE of b1 holds b2 on b3 );

:: deftheorem Def12 defines up-3-rank INCPROJ:def 12 :
for b1 being IncProjStr holds
( b1 is up-3-rank iff for b2 being LINE of b1 ex b3, b4, b5 being POINT of b1 st
( b3 <> b4 & b4 <> b5 & b5 <> b3 & b3 on b2 & b4 on b2 & b5 on b2 ) );

:: deftheorem Def13 defines Vebleian INCPROJ:def 13 :
for b1 being IncProjStr holds
( b1 is Vebleian iff for b2, b3, b4, b5, b6, b7 being POINT of b1
for b8, b9, b10, b11 being LINE of b1 st b2 on b8 & b3 on b8 & b4 on b9 & b5 on b9 & b6 on b8 & b6 on b9 & b2 on b10 & b4 on b10 & b3 on b11 & b5 on b11 & not b6 on b10 & not b6 on b11 & b8 <> b9 holds
ex b12 being POINT of b1 st
( b12 on b10 & b12 on b11 ) );

registration
let c1 be CollProjectiveSpace;
cluster IncProjSp_of a1 -> strict partial linear up-2-dimensional up-3-rank Vebleian ;
coherence
( IncProjSp_of c1 is partial & IncProjSp_of c1 is linear & IncProjSp_of c1 is up-2-dimensional & IncProjSp_of c1 is up-3-rank & IncProjSp_of c1 is Vebleian )
proof end;
end;

registration
cluster strict partial linear up-2-dimensional up-3-rank Vebleian IncProjStr ;
existence
ex b1 being IncProjStr st
( b1 is strict & b1 is partial & b1 is linear & b1 is up-2-dimensional & b1 is up-3-rank & b1 is Vebleian )
proof end;
end;

definition
mode IncProjSp is partial linear up-2-dimensional up-3-rank Vebleian IncProjStr ;
end;

registration
let c1 be CollProjectiveSpace;
cluster IncProjSp_of a1 -> strict partial linear up-2-dimensional up-3-rank Vebleian ;
coherence
( IncProjSp_of c1 is partial & IncProjSp_of c1 is linear & IncProjSp_of c1 is up-2-dimensional & IncProjSp_of c1 is up-3-rank & IncProjSp_of c1 is Vebleian ) ;
end;

definition
let c1 be IncProjSp;
attr a1 is 2-dimensional means :Def14: :: INCPROJ:def 14
for b1, b2 being LINE of a1 ex b3 being POINT of a1 st
( b3 on b1 & b3 on b2 );
end;

:: deftheorem Def14 defines 2-dimensional INCPROJ:def 14 :
for b1 being IncProjSp holds
( b1 is 2-dimensional iff for b2, b3 being LINE of b1 ex b4 being POINT of b1 st
( b4 on b2 & b4 on b3 ) );

notation
let c1 be IncProjSp;
antonym up-3-dimensional c1 for 2-dimensional c1;
end;

definition
let c1 be IncProjSp;
canceled;
attr a1 is at_most-3-dimensional means :Def16: :: INCPROJ:def 16
for b1 being POINT of a1
for b2, b3 being LINE of a1 ex b4, b5 being POINT of a1ex b6 being LINE of a1 st
( b1 on b6 & b4 on b6 & b5 on b6 & b4 on b2 & b5 on b3 );
end;

:: deftheorem Def15 INCPROJ:def 15 :
canceled;

:: deftheorem Def16 defines at_most-3-dimensional INCPROJ:def 16 :
for b1 being IncProjSp holds
( b1 is at_most-3-dimensional iff for b2 being POINT of b1
for b3, b4 being LINE of b1 ex b5, b6 being POINT of b1ex b7 being LINE of b1 st
( b2 on b7 & b5 on b7 & b6 on b7 & b5 on b3 & b6 on b4 ) );

definition
let c1 be IncProjSp;
attr a1 is 3-dimensional means :: INCPROJ:def 17
( a1 is at_most-3-dimensional & not a1 is 2-dimensional );
end;

:: deftheorem Def17 defines 3-dimensional INCPROJ:def 17 :
for b1 being IncProjSp holds
( b1 is 3-dimensional iff ( b1 is at_most-3-dimensional & not b1 is 2-dimensional ) );

definition
let c1 be IncProjSp;
attr a1 is Fanoian means :Def18: :: INCPROJ:def 18
for b1, b2, b3, b4, b5, b6, b7 being POINT of a1
for b8, b9, b10, b11, b12, b13, b14 being LINE of a1 st not b2 on b8 & not b3 on b8 & not b1 on b9 & not b4 on b9 & not b1 on b10 & not b3 on b10 & not b2 on b11 & not b4 on b11 & b5,b1,b4 on b8 & b5,b2,b3 on b9 & b6,b2,b4 on b10 & b6,b1,b3 on b11 & b7,b1,b2 on b12 & b7,b3,b4 on b13 & b5,b6 on b14 holds
not b7 on b14;
end;

:: deftheorem Def18 defines Fanoian INCPROJ:def 18 :
for b1 being IncProjSp holds
( b1 is Fanoian iff for b2, b3, b4, b5, b6, b7, b8 being POINT of b1
for b9, b10, b11, b12, b13, b14, b15 being LINE of b1 st not b3 on b9 & not b4 on b9 & not b2 on b10 & not b5 on b10 & not b2 on b11 & not b4 on b11 & not b3 on b12 & not b5 on b12 & b6,b2,b5 on b9 & b6,b3,b4 on b10 & b7,b3,b5 on b11 & b7,b2,b4 on b12 & b8,b2,b3 on b13 & b8,b4,b5 on b14 & b6,b7 on b15 holds
not b8 on b15 );

definition
let c1 be IncProjSp;
attr a1 is Desarguesian means :Def19: :: INCPROJ:def 19
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being POINT of a1
for b11, b12, b13, b14, b15, b16, b17, b18, b19 being LINE of a1 st b1,b2,b3 on b11 & b1,b5,b4 on b12 & b1,b7,b6 on b13 & b7,b5,b10 on b14 & b7,b8,b3 on b15 & b5,b9,b3 on b16 & b10,b4,b6 on b17 & b2,b8,b6 on b18 & b2,b9,b4 on b19 & b11,b12,b13 are_mutually_different & b1 <> b3 & b1 <> b5 & b1 <> b7 & b1 <> b2 & b1 <> b4 & b1 <> b6 & b3 <> b2 & b5 <> b4 & b7 <> b6 holds
ex b20 being LINE of a1 st b8,b9,b10 on b20;
end;

:: deftheorem Def19 defines Desarguesian INCPROJ:def 19 :
for b1 being IncProjSp holds
( b1 is Desarguesian iff for b2, b3, b4, b5, b6, b7, b8, b9, b10, b11 being POINT of b1
for b12, b13, b14, b15, b16, b17, b18, b19, b20 being LINE of b1 st b2,b3,b4 on b12 & b2,b6,b5 on b13 & b2,b8,b7 on b14 & b8,b6,b11 on b15 & b8,b9,b4 on b16 & b6,b10,b4 on b17 & b11,b5,b7 on b18 & b3,b9,b7 on b19 & b3,b10,b5 on b20 & b12,b13,b14 are_mutually_different & b2 <> b4 & b2 <> b6 & b2 <> b8 & b2 <> b3 & b2 <> b5 & b2 <> b7 & b4 <> b3 & b6 <> b5 & b8 <> b7 holds
ex b21 being LINE of b1 st b9,b10,b11 on b21 );

definition
let c1 be IncProjSp;
attr a1 is Pappian means :Def20: :: INCPROJ:def 20
for b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 being POINT of a1
for b11, b12, b13, b14, b15, b16, b17, b18, b19 being LINE of a1 st b1,b2,b3,b4 are_mutually_different & b1,b5,b6,b7 are_mutually_different & b13 <> b16 & b1 on b13 & b1 on b16 & b3,b7,b8 on b11 & b4,b5,b9 on b14 & b2,b6,b10 on b17 & b2,b7,b9 on b12 & b4,b6,b8 on b15 & b3,b5,b10 on b18 & b5,b6,b7 on b13 & b2,b3,b4 on b16 & b8,b9 on b19 holds
b10 on b19;
end;

:: deftheorem Def20 defines Pappian INCPROJ:def 20 :
for b1 being IncProjSp holds
( b1 is Pappian iff for b2, b3, b4, b5, b6, b7, b8, b9, b10, b11 being POINT of b1
for b12, b13, b14, b15, b16, b17, b18, b19, b20 being LINE of b1 st b2,b3,b4,b5 are_mutually_different & b2,b6,b7,b8 are_mutually_different & b14 <> b17 & b2 on b14 & b2 on b17 & b4,b8,b9 on b12 & b5,b6,b10 on b15 & b3,b7,b11 on b18 & b3,b8,b10 on b13 & b5,b7,b9 on b16 & b4,b6,b11 on b19 & b6,b7,b8 on b14 & b3,b4,b5 on b17 & b9,b10 on b20 holds
b11 on b20 );

registration
cluster up-3-dimensional at_most-3-dimensional Fanoian Desarguesian IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is Desarguesian & b1 is Fanoian & b1 is at_most-3-dimensional & not b1 is 2-dimensional )
proof end;
end;

registration
cluster up-3-dimensional at_most-3-dimensional Fanoian Pappian IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is Pappian & b1 is Fanoian & b1 is at_most-3-dimensional & not b1 is 2-dimensional )
proof end;
end;

registration
cluster 2-dimensional Fanoian Desarguesian IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is Desarguesian & b1 is Fanoian & b1 is 2-dimensional )
proof end;
end;

registration
cluster 2-dimensional Fanoian Pappian IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is Pappian & b1 is Fanoian & b1 is 2-dimensional )
proof end;
end;