:: INCPROJ semantic presentation

begin


definition
let CPS be proper CollSp;
:: original: LINE
redefine mode LINE of CPS ->  Subset of CPS;
coherence
 for b1 being LINE of CPS holds b1 is Subset of CPS
proof
let x be LINE of CPS; ::_thesis: x is Subset of CPS
 x c= the carrier of CPS
proof
consider a, b being Point of CPS such that
 a <> b and
A1: x = Line (a,b) by COLLSP:def_7;
now__::_thesis:_for_z_being_set_st_z_in_x_holds_
z_in_the_carrier_of_CPS
let z be set ; ::_thesis: ( z in x implies z in the carrier of CPS )
assume  z in x ; ::_thesis: z in the carrier of CPS
then  z in  {  p where p is Point of CPS : a,b,p is_collinear  }  by A1, COLLSP:def_5;
then  ex p being Point of CPS st
( z = p & a,b,p is_collinear ) ;
hence  z in the carrier of CPS ; ::_thesis: verum
end;
hence  x c= the carrier of CPS by TARSKI:def_3; ::_thesis: verum
end;
hence  x is Subset of CPS ; ::_thesis: verum
end;
end;

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

:: deftheorem  defines ProjectiveLines INCPROJ:def_1_:_
 for CPS being proper CollSp holds ProjectiveLines CPS =  {  B where B is Subset of CPS : B is LINE of CPS  }  ;

registration
let CPS be proper CollSp;
cluster ProjectiveLines CPS ->  non empty ;
coherence
 not ProjectiveLines CPS is empty
proof
set x = the LINE of CPS;
 the LINE of CPS in ProjectiveLines CPS ;
hence  not ProjectiveLines CPS is empty ; ::_thesis: verum
end;
end;

theorem Th1: :: INCPROJ:1
for CPS being proper CollSp
for x being set holds
( x is LINE of CPS iff x is Element of ProjectiveLines CPS )
proof
let CPS be proper CollSp; ::_thesis: for x being set holds
( x is LINE of CPS iff x is Element of ProjectiveLines CPS )
let x be set ; ::_thesis: ( x is LINE of CPS iff x is Element of ProjectiveLines CPS )
hereby  ::_thesis: ( x is Element of ProjectiveLines CPS implies x is LINE of CPS )
assume  x is LINE of CPS ; ::_thesis: x is Element of ProjectiveLines CPS
then  x in  {  B where B is Subset of CPS : B is LINE of CPS  }  ;
hence  x is Element of ProjectiveLines CPS ; ::_thesis: verum
end;
assume  x is Element of ProjectiveLines CPS ; ::_thesis: x is LINE of CPS
then  x in ProjectiveLines CPS ;
then  ex B being Subset of CPS st
( x = B & B is LINE of CPS ) ;
hence  x is LINE of CPS ; ::_thesis: verum
end;

definition
let CPS be proper CollSp;
func Proj_Inc CPS ->  Relation of the carrier of CPS,(ProjectiveLines CPS) means :Def2: :: INCPROJ:def 2
 for x, y being set holds
( [x,y] in it iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) );
existence
 ex b1 being Relation of the carrier of CPS,(ProjectiveLines CPS) st
for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) )
proof
defpred S1[ set , set ] means  ex Y being set st
( $2 = Y & $1 in Y );
 ex IT being Relation of the carrier of CPS,(ProjectiveLines CPS) st
for x, y being set holds
( [x,y] in IT iff ( x in the carrier of CPS & y in ProjectiveLines CPS & S1[x,y] ) ) from RELSET_1:sch_1();
hence  ex b1 being Relation of the carrier of CPS,(ProjectiveLines CPS) st
for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of the carrier of CPS,(ProjectiveLines CPS) st ( for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ) holds
b1 = b2
proof
let R1, R2 be Relation of the carrier of CPS,(ProjectiveLines CPS); ::_thesis: ( ( for x, y being set holds
( [x,y] in R1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ) & ( for x, y being set holds
( [x,y] in R2 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ) implies R1 = R2 )
assume that
A1: for x, y being set holds
( [x,y] in R1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) and
A2: for x, y being set holds
( [x,y] in R2 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ; ::_thesis: R1 = R2
now__::_thesis:_for_x,_y_being_set_holds_
(_[x,y]_in_R1_iff_[x,y]_in_R2_)
let x, y be set ; ::_thesis: ( [x,y] in R1 iff [x,y] in R2 )
A3: now__::_thesis:_(_[x,y]_in_R2_implies_[x,y]_in_R1_)
assume A4: [x,y] in R2 ; ::_thesis: [x,y] in R1
then A5: ex Y being set st
( y = Y & x in Y ) by A2;
 ( x in the carrier of CPS & y in ProjectiveLines CPS ) by A2, A4;
hence  [x,y] in R1 by A1, A5; ::_thesis: verum
end;
now__::_thesis:_(_[x,y]_in_R1_implies_[x,y]_in_R2_)
assume A6: [x,y] in R1 ; ::_thesis: [x,y] in R2
then A7: ex Y being set st
( y = Y & x in Y ) by A1;
 ( x in the carrier of CPS & y in ProjectiveLines CPS ) by A1, A6;
hence  [x,y] in R2 by A2, A7; ::_thesis: verum
end;
hence  ( [x,y] in R1 iff [x,y] in R2 ) by A3; ::_thesis: verum
end;
hence  R1 = R2 by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Proj_Inc INCPROJ:def_2_:_
 for CPS being proper CollSp
for b2 being Relation of the carrier of CPS,(ProjectiveLines CPS) holds
( b2 = Proj_Inc CPS iff for x, y being set holds
( [x,y] in b2 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) );

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

:: deftheorem  defines IncProjSp_of INCPROJ:def_3_:_
 for CPS being proper CollSp holds IncProjSp_of CPS = IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);

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

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

theorem :: INCPROJ:3
for CPS being proper CollSp
for x being set holds
( x is Point of CPS iff x is POINT of (IncProjSp_of CPS) ) ;

theorem :: INCPROJ:4
for CPS being proper CollSp
for x being set holds
( x is LINE of CPS iff x is LINE of (IncProjSp_of CPS) ) by Th1;


theorem Th5: :: INCPROJ:5
for CPS being proper CollSp
for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS)
for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
proof
let CPS be proper CollSp; ::_thesis: for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS)
for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
let p be POINT of (IncProjSp_of CPS); ::_thesis: for P being LINE of (IncProjSp_of CPS)
for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
let P be LINE of (IncProjSp_of CPS); ::_thesis: for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
let p9 be Point of CPS; ::_thesis: for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
let P9 be LINE of CPS; ::_thesis: ( p = p9 & P = P9 implies ( p on P iff p9 in P9 ) )
reconsider P99 = P9 as LINE of (IncProjSp_of CPS) by Th1;
reconsider P999 = P99 as Element of ProjectiveLines CPS ;
assume A1: ( p = p9 & P = P9 ) ; ::_thesis: ( p on P iff p9 in P9 )
hereby  ::_thesis: ( p9 in P9 implies p on P )
assume  p on P ; ::_thesis: p9 in P9
then  [p9,P9] in Proj_Inc CPS by A1, INCSP_1:def_1;
then  ex Y being set st
( P9 = Y & p9 in Y ) by Def2;
hence  p9 in P9 ; ::_thesis: verum
end;
assume  p9 in P9 ; ::_thesis: p on P
then  [p9,P999] in Proj_Inc CPS by Def2;
hence  p on P by A1, INCSP_1:def_1; ::_thesis: verum
end;

theorem Th6: :: INCPROJ:6
for CPS being proper CollSp ex a9, b9, c9 being Point of CPS st
( a9 <> b9 & b9 <> c9 & c9 <> a9 )
proof
let CPS be proper CollSp; ::_thesis: ex a9, b9, c9 being Point of CPS st
( a9 <> b9 & b9 <> c9 & c9 <> a9 )
consider a99, b99, c99 being Point of CPS such that
A1: not a99,b99,c99 is_collinear by COLLSP:def_6;
A2: c99 <> a99 by A1, COLLSP:2;
 ( a99 <> b99 & b99 <> c99 ) by A1, COLLSP:2;
hence  ex a9, b9, c9 being Point of CPS st
( a9 <> b9 & b9 <> c9 & c9 <> a9 ) by A2; ::_thesis: verum
end;

theorem Th7: :: INCPROJ:7
for CPS being proper CollSp
for a9 being Point of CPS ex b9 being Point of CPS st a9 <> b9
proof
let CPS be proper CollSp; ::_thesis: for a9 being Point of CPS ex b9 being Point of CPS st a9 <> b9
let a9 be Point of CPS; ::_thesis: ex b9 being Point of CPS st a9 <> b9
consider p9, q9, r9 being Point of CPS such that
A1: p9 <> q9 and
 q9 <> r9 and
 r9 <> p9 by Th6;
 ( a9 <> p9 or a9 <> q9 ) by A1;
hence  ex b9 being Point of CPS st a9 <> b9 ; ::_thesis: verum
end;

theorem Th8: :: INCPROJ:8
for CPS being proper CollSp
for p, q being POINT of (IncProjSp_of CPS)
for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q
proof
let CPS be proper CollSp; ::_thesis: for p, q being POINT of (IncProjSp_of CPS)
for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q
let p, q be POINT of (IncProjSp_of CPS); ::_thesis: for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q
let P, Q be LINE of (IncProjSp_of CPS); ::_thesis: ( p on P & q on P & p on Q & q on Q & not p = q implies P = Q )
reconsider p9 = p, q9 = q as Point of CPS ;
reconsider P9 = P, Q9 = Q as LINE of CPS by Th1;
assume that
A1: ( p on P & q on P ) and
A2: ( p on Q & q on Q ) and
A3: p <> q ; ::_thesis: P = Q
A4: ( p9 in Q9 & q9 in Q9 ) by A2, Th5;
 ( p9 in P9 & q9 in P9 ) by A1, Th5;
hence  P = Q by A3, A4, COLLSP:20; ::_thesis: verum
end;

theorem Th9: :: INCPROJ:9
for CPS being proper CollSp
for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
proof
let CPS be proper CollSp; ::_thesis: for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
let p, q be POINT of (IncProjSp_of CPS); ::_thesis: ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
reconsider p9 = p, q9 = q as Point of CPS ;
A1: now__::_thesis:_(_p9_=_q9_implies_ex_P_being_LINE_of_(IncProjSp_of_CPS)_st_
(_p_on_P_&_q_on_P_)_)
consider r9 being Point of CPS such that
A2: p9 <> r9 by Th7;
consider P9 being LINE of CPS such that
A3: p9 in P9 and
 r9 in P9 by A2, COLLSP:15;
reconsider P = P9 as LINE of (IncProjSp_of CPS) by Th1;
assume A4: p9 = q9 ; ::_thesis: ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
 p on P by A3, Th5;
hence  ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) by A4; ::_thesis: verum
end;
now__::_thesis:_(_p9_<>_q9_implies_ex_P_being_LINE_of_(IncProjSp_of_CPS)_st_
(_p_on_P_&_q_on_P_)_)
assume  p9 <> q9 ; ::_thesis: ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
then consider P9 being LINE of CPS such that
A5: ( p9 in P9 & q9 in P9 ) by COLLSP:15;
reconsider P = P9 as LINE of (IncProjSp_of CPS) by Th1;
 ( p on P & q on P ) by A5, Th5;
hence  ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) ; ::_thesis: verum
end;
hence  ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) by A1; ::_thesis: verum
end;

theorem Th10: :: INCPROJ:10
for CPS being proper CollSp
for a, b, c being POINT of (IncProjSp_of CPS)
for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 is_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
proof
let CPS be proper CollSp; ::_thesis: for a, b, c being POINT of (IncProjSp_of CPS)
for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 is_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
let a, b, c be POINT of (IncProjSp_of CPS); ::_thesis: for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 is_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
let a9, b9, c9 be Point of CPS; ::_thesis: ( a = a9 & b = b9 & c = c9 implies ( a9,b9,c9 is_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) ) )
assume that
A1: a = a9 and
A2: b = b9 and
A3: c = c9 ; ::_thesis: ( a9,b9,c9 is_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
hereby  ::_thesis: ( ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) implies a9,b9,c9 is_collinear )
assume A4: a9,b9,c9 is_collinear ; ::_thesis: ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )
A5: now__::_thesis:_(_a9_<>_b9_implies_ex_P_being_LINE_of_(IncProjSp_of_CPS)_st_
(_a_on_P_&_b_on_P_&_c_on_P_)_)
set X = Line (a9,b9);
assume  a9 <> b9 ; ::_thesis: ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )
then reconsider P9 = Line (a9,b9) as LINE of CPS by COLLSP:def_7;
reconsider P = P9 as LINE of (IncProjSp_of CPS) by Th1;
 a9 in Line (a9,b9) by COLLSP:10;
then A6: a on P by A1, Th5;
 b9 in Line (a9,b9) by COLLSP:10;
then A7: b on P by A2, Th5;
 c9 in Line (a9,b9) by A4, COLLSP:11;
then  c on P by A3, Th5;
hence  ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) by A6, A7; ::_thesis: verum
end;
now__::_thesis:_(_a9_=_b9_implies_ex_P_being_LINE_of_(IncProjSp_of_CPS)_st_
(_a_on_P_&_b_on_P_&_c_on_P_)_)
assume A8: a9 = b9 ; ::_thesis: ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )
 ex P being LINE of (IncProjSp_of CPS) st
( b on P & c on P ) by Th9;
hence  ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) by A1, A2, A8; ::_thesis: verum
end;
hence  ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) by A5; ::_thesis: verum
end;
given P being LINE of (IncProjSp_of CPS) such that A9: ( a on P & b on P ) and
A10: c on P ; ::_thesis: a9,b9,c9 is_collinear
reconsider P9 = P as LINE of CPS by Th1;
A11: c9 in P9 by A3, A10, Th5;
 ( a9 in P9 & b9 in P9 ) by A1, A2, A9, Th5;
hence  a9,b9,c9 is_collinear by A11, COLLSP:16; ::_thesis: verum
end;

theorem Th11: :: INCPROJ:11
for CPS being proper CollSp holds
not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P
proof
let CPS be proper CollSp; ::_thesis: not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P
consider p9, q9, r9 being Point of CPS such that
A1: not p9,q9,r9 is_collinear by COLLSP:def_6;
set X = Line (p9,q9);
 p9 <> q9 by A1, COLLSP:2;
then reconsider P9 = Line (p9,q9) as LINE of CPS by COLLSP:def_7;
reconsider P = P9 as LINE of (IncProjSp_of CPS) by Th1;
reconsider r = r9 as POINT of (IncProjSp_of CPS) ;
 not r on P
proof
assume  r on P ; ::_thesis: contradiction
then  r9 in Line (p9,q9) by Th5;
hence  contradiction by A1, COLLSP:11; ::_thesis: verum
end;
hence  not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P ; ::_thesis: verum
end;


theorem Th12: :: INCPROJ:12
for CPS being CollProjectiveSpace
for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
proof
let CPS be CollProjectiveSpace; ::_thesis: for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
let P be LINE of (IncProjSp_of CPS); ::_thesis: ex a, b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
reconsider P9 = P as LINE of CPS by Th1;
consider a99, b99 being Point of CPS such that
A1: a99 <> b99 and
A2: P9 = Line (a99,b99) by COLLSP:def_7;
consider c9 being Point of CPS such that
A3: ( a99 <> c9 & b99 <> c9 ) and
A4: a99,b99,c9 is_collinear by ANPROJ_2:def_10;
reconsider a = a99, b = b99, c = c9 as POINT of (IncProjSp_of CPS) ;
take  a ; ::_thesis: ex b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
take  b ; ::_thesis: ex c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
take  c ; ::_thesis: ( a <> b & b <> c & c <> a & a on P & b on P & c on P )
thus  ( a <> b & b <> c & c <> a ) by A1, A3; ::_thesis: ( a on P & b on P & c on P )
 a99 in P9 by A2, COLLSP:10;
then A5: a on P by Th5;
 b99 in P9 by A2, COLLSP:10;
then A6: b on P by Th5;
 ex Q being LINE of (IncProjSp_of CPS) st
( a on Q & b on Q & c on Q ) by A4, Th10;
hence  ( a on P & b on P & c on P ) by A1, A5, A6, Th8; ::_thesis: verum
end;

theorem Th13: :: INCPROJ:13
for CPS being CollProjectiveSpace
for a, b, c, d, p being POINT of (IncProjSp_of CPS)
for M, N, P, Q being LINE of (IncProjSp_of CPS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )
proof
let CPS be CollProjectiveSpace; ::_thesis: for a, b, c, d, p being POINT of (IncProjSp_of CPS)
for M, N, P, Q being LINE of (IncProjSp_of CPS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )
let a, b, c, d, p be POINT of (IncProjSp_of CPS); ::_thesis: for M, N, P, Q being LINE of (IncProjSp_of CPS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )
let M, N, P, Q be LINE of (IncProjSp_of CPS); ::_thesis: ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N implies ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q ) )
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: ( p on M & p on N ) and
A6: a on P and
A7: c on P and
A8: b on Q and
A9: d on Q and
A10: not p on P and
A11: not p on Q and
A12: M <> N ; ::_thesis: ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p as Point of CPS ;
 ( b9,p9,a9 is_collinear & p9,d9,c9 is_collinear ) by A1, A2, A3, A4, A5, Th10;
then consider q9 being Point of CPS such that
A13: b9,d9,q9 is_collinear and
A14: a9,c9,q9 is_collinear by ANPROJ_2:def_9;
reconsider q = q9 as POINT of (IncProjSp_of CPS) ;
A15: ex P2 being LINE of (IncProjSp_of CPS) st
( b on P2 & d on P2 & q on P2 ) by A13, Th10;
 b <> d by A2, A4, A5, A8, A11, A12, Th8;
then A16: q on Q by A8, A9, A15, Th8;
A17: ex P1 being LINE of (IncProjSp_of CPS) st
( a on P1 & c on P1 & q on P1 ) by A14, Th10;
 a <> c by A1, A3, A5, A6, A10, A12, Th8;
then  q on P by A6, A7, A17, Th8;
hence  ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q ) by A16; ::_thesis: verum
end;

theorem Th14: :: INCPROJ:14
for CPS being CollProjectiveSpace st ( for a9, b9, c9, d9 being Point of CPS ex p9 being Point of CPS st
( a9,b9,p9 is_collinear & c9,d9,p9 is_collinear ) ) holds
for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N )
proof
let CPS be CollProjectiveSpace; ::_thesis: ( ( for a9, b9, c9, d9 being Point of CPS ex p9 being Point of CPS st
( a9,b9,p9 is_collinear & c9,d9,p9 is_collinear ) ) implies for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N ) )
assume A1: for a9, b9, c9, d9 being Point of CPS ex p9 being Point of CPS st
( a9,b9,p9 is_collinear & c9,d9,p9 is_collinear ) ; ::_thesis: for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N )
let M, N be LINE of (IncProjSp_of CPS); ::_thesis: ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N )
reconsider M9 = M, N9 = N as LINE of CPS by Th1;
consider a9, b9 being Point of CPS such that
 a9 <> b9 and
A2: M9 = Line (a9,b9) by COLLSP:def_7;
consider c9, d9 being Point of CPS such that
 c9 <> d9 and
A3: N9 = Line (c9,d9) by COLLSP:def_7;
consider p9 being Point of CPS such that
A4: a9,b9,p9 is_collinear and
A5: c9,d9,p9 is_collinear by A1;
reconsider q = p9 as POINT of (IncProjSp_of CPS) ;
 p9 in N9 by A3, A5, COLLSP:11;
then A6: q on N by Th5;
 p9 in M9 by A2, A4, COLLSP:11;
then  q on M by Th5;
hence  ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N ) by A6; ::_thesis: verum
end;

theorem Th15: :: INCPROJ:15
for CPS being CollProjectiveSpace st ex p, p1, r, r1 being Point of CPS st
for s being Point of CPS holds
( not p,p1,s is_collinear or not r,r1,s is_collinear ) holds
ex M, N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )
proof
let CPS be CollProjectiveSpace; ::_thesis: ( ex p, p1, r, r1 being Point of CPS st
for s being Point of CPS holds
( not p,p1,s is_collinear or not r,r1,s is_collinear ) implies ex M, N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N ) )
given p, p1, r, r1 being Point of CPS such that A1: for s being Point of CPS holds
( not p,p1,s is_collinear or not r,r1,s is_collinear ) ; ::_thesis: ex M, N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )
set M99 = Line (p,p1);
set N99 = Line (r,r1);
 ( p <> p1 & r <> r1 )
proof
A2: now__::_thesis:_not_p_=_p1
assume  p = p1 ; ::_thesis: contradiction
then A3: p,p1,r1 is_collinear by COLLSP:2;
 r,r1,r1 is_collinear by COLLSP:2;
hence  contradiction by A1, A3; ::_thesis: verum
end;
A4: now__::_thesis:_not_r_=_r1
assume  r = r1 ; ::_thesis: contradiction
then  ( p,p1,p1 is_collinear & r,r1,p1 is_collinear ) by COLLSP:2;
hence  contradiction by A1; ::_thesis: verum
end;
assume  ( not p <> p1 or not r <> r1 ) ; ::_thesis: contradiction
hence  contradiction by A2, A4; ::_thesis: verum
end;
then reconsider M9 = Line (p,p1), N9 = Line (r,r1) as LINE of CPS by COLLSP:def_7;
reconsider M = M9, N = N9 as LINE of (IncProjSp_of CPS) by Th1;
take  M ; ::_thesis: ex N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )
take  N ; ::_thesis: for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )
thus  for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N ) ::_thesis: verum
proof
assume  ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N ) ; ::_thesis: contradiction
then consider q being POINT of (IncProjSp_of CPS) such that
A5: q on M and
A6: q on N ;
reconsider q9 = q as Point of CPS ;
 q9 in Line (r,r1) by A6, Th5;
then A7: r,r1,q9 is_collinear by COLLSP:11;
 q9 in Line (p,p1) by A5, Th5;
then  p,p1,q9 is_collinear by COLLSP:11;
hence  contradiction by A1, A7; ::_thesis: verum
end;
end;

theorem Th16: :: INCPROJ:16
for CPS being CollProjectiveSpace st ( for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of CPS st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) ) holds
for a being POINT of (IncProjSp_of CPS)
for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )
proof
let CPS be CollProjectiveSpace; ::_thesis: ( ( for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of CPS st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) ) implies for a being POINT of (IncProjSp_of CPS)
for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N ) )
assume A1: for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of CPS st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) ; ::_thesis: for a being POINT of (IncProjSp_of CPS)
for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )
let a be POINT of (IncProjSp_of CPS); ::_thesis: for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )
let M, N be LINE of (IncProjSp_of CPS); ::_thesis: ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )
reconsider M9 = M, N9 = N as LINE of CPS by Th1;
reconsider a9 = a as Point of CPS ;
consider p, q being Point of CPS such that
 p <> q and
A2: M9 = Line (p,q) by COLLSP:def_7;
consider p1, q1 being Point of CPS such that
 p1 <> q1 and
A3: N9 = Line (p1,q1) by COLLSP:def_7;
consider b9, c9 being Point of CPS such that
A4: p,q,b9 is_collinear and
A5: p1,q1,c9 is_collinear and
A6: a9,b9,c9 is_collinear by A1;
reconsider b = b9, c = c9 as POINT of (IncProjSp_of CPS) ;
 b9 in M9 by A2, A4, COLLSP:11;
then A7: b on M by Th5;
 c9 in N9 by A3, A5, COLLSP:11;
then A8: c on N by Th5;
 ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S ) by A6, Th10;
hence  ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N ) by A7, A8; ::_thesis: verum
end;

theorem Th17: :: INCPROJ:17
for CPS being CollProjectiveSpace st ( for p1, r2, q, r1, q1, p, r being Point of CPS st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear ) holds
for p, q, r, s, a, b, c being POINT of (IncProjSp_of CPS)
for L, Q, R, S, A, B, C being LINE of (IncProjSp_of CPS) st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C
proof
let CPS be CollProjectiveSpace; ::_thesis: ( ( for p1, r2, q, r1, q1, p, r being Point of CPS st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear ) implies for p, q, r, s, a, b, c being POINT of (IncProjSp_of CPS)
for L, Q, R, S, A, B, C being LINE of (IncProjSp_of CPS) st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C )
assume A1: for p1, r2, q, r1, q1, p, r being Element of CPS st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear ; ::_thesis: for p, q, r, s, a, b, c being POINT of (IncProjSp_of CPS)
for L, Q, R, S, A, B, C being LINE of (IncProjSp_of CPS) st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C
let p, q, r, s, a, b, c be POINT of (IncProjSp_of CPS); ::_thesis: for L, Q, R, S, A, B, C being LINE of (IncProjSp_of CPS) st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C
let L, Q, R, S, A, B, C be LINE of (IncProjSp_of CPS); ::_thesis: ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C implies not c on C )
assume that
A2: not q on L and
A3: not r on L and
A4: not p on Q and
A5: not s on Q and
A6: not p on R and
A7: not r on R and
A8: {a,p,s} on L and
A9: {a,q,r} on Q and
A10: {b,q,s} on R and
A11: {b,p,r} on S and
A12: {c,p,q} on A and
A13: {c,r,s} on B and
A14: {a,b} on C ; ::_thesis: not c on C
reconsider p9 = p, q9 = q, r9 = r, s9 = s, a9 = a, b9 = b, c9 = c as Point of CPS ;
A15: ( p on L & s on L ) by A8, INCSP_1:2;
A16: s on R by A10, INCSP_1:2;
A17: now__::_thesis:_(_p9,r9,s9_is_collinear_implies_(_s_on_S_&_contradiction_)_)
assume  p9,r9,s9 is_collinear ; ::_thesis: ( s on S & contradiction )
then A18: ex K being LINE of (IncProjSp_of CPS) st
( p on K & r on K & s on K ) by Th10;
hence  s on S by A3, A6, A15, A16, Th8; ::_thesis: contradiction
thus  contradiction by A3, A6, A15, A16, A18, Th8; ::_thesis: verum
end;
A19: now__::_thesis:_(_p9,s9,q9_is_collinear_implies_(_p_on_R_&_contradiction_)_)
assume  p9,s9,q9 is_collinear ; ::_thesis: ( p on R & contradiction )
then A20: ex K being LINE of (IncProjSp_of CPS) st
( p on K & s on K & q on K ) by Th10;
hence  p on R by A2, A15, A16, Th8; ::_thesis: contradiction
thus  contradiction by A2, A6, A15, A16, A20, Th8; ::_thesis: verum
end;
 a on L by A8, INCSP_1:2;
then A21: p9,s9,a9 is_collinear by A15, Th10;
assume A22: c on C ; ::_thesis: contradiction
 ( a on C & b on C ) by A14, INCSP_1:1;
then A23: a9,b9,c9 is_collinear by A22, Th10;
A24: ( q on Q & r on Q ) by A9, INCSP_1:2;
A25: q on R by A10, INCSP_1:2;
A26: now__::_thesis:_(_p9,r9,q9_is_collinear_implies_(_q_on_S_&_contradiction_)_)
assume  p9,r9,q9 is_collinear ; ::_thesis: ( q on S & contradiction )
then A27: ex K being LINE of (IncProjSp_of CPS) st
( p on K & r on K & q on K ) by Th10;
hence  q on S by A4, A7, A24, A25, Th8; ::_thesis: contradiction
thus  contradiction by A4, A7, A24, A25, A27, Th8; ::_thesis: verum
end;
A28: now__::_thesis:_(_r9,s9,q9_is_collinear_implies_(_r_on_R_&_contradiction_)_)
assume  r9,s9,q9 is_collinear ; ::_thesis: ( r on R & contradiction )
then A29: ex K being LINE of (IncProjSp_of CPS) st
( r on K & s on K & q on K ) by Th10;
hence  r on R by A5, A24, A25, Th8; ::_thesis: contradiction
thus  contradiction by A5, A7, A24, A25, A29, Th8; ::_thesis: verum
end;
 a on Q by A9, INCSP_1:2;
then A30: r9,q9,a9 is_collinear by A24, Th10;
A31: r on S by A11, INCSP_1:2;
 ( b on S & p on S ) by A11, INCSP_1:2;
then A32: p9,r9,b9 is_collinear by A31, Th10;
A33: s on B by A13, INCSP_1:2;
 ( c on B & r on B ) by A13, INCSP_1:2;
then A34: r9,s9,c9 is_collinear by A33, Th10;
A35: q on A by A12, INCSP_1:2;
 ( c on A & p on A ) by A12, INCSP_1:2;
then A36: p9,q9,c9 is_collinear by A35, Th10;
 b on R by A10, INCSP_1:2;
then  s9,q9,b9 is_collinear by A25, A16, Th10;
hence  contradiction by A1, A23, A32, A21, A30, A36, A34, A26, A17, A19, A28; ::_thesis: verum
end;

theorem Th18: :: INCPROJ:18
for CPS being CollProjectiveSpace st ( for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear ) holds
for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of (IncProjSp_of CPS)
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of (IncProjSp_of CPS) st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O
proof
let CPS be CollProjectiveSpace; ::_thesis: ( ( for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear ) implies for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of (IncProjSp_of CPS)
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of (IncProjSp_of CPS) st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O )
assume A1: for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of CPS st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear ; ::_thesis: for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of (IncProjSp_of CPS)
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of (IncProjSp_of CPS) st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of (IncProjSp_of CPS); ::_thesis: for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of (IncProjSp_of CPS) st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of (IncProjSp_of CPS); ::_thesis: ( {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 implies ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O )
assume that
A2: {o,b1,a1} on C1 and
A3: {o,a2,b2} on C2 and
A4: {o,a3,b3} on C3 and
A5: {a3,a2,t} on A1 and
A6: {a3,r,a1} on A2 and
A7: {a2,s,a1} on A3 and
A8: {t,b2,b3} on B1 and
A9: {b1,r,b3} on B2 and
A10: {b1,s,b2} on B3 and
A11: C1,C2,C3 are_mutually_different and
A12: ( o <> a1 & o <> a2 & o <> a3 ) and
A13: o <> b1 and
A14: o <> b2 and
A15: o <> b3 and
A16: ( a1 <> b1 & a2 <> b2 & a3 <> b3 ) ; ::_thesis: ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O
reconsider o9 = o, b19 = b1, a19 = a1, b29 = b2, a29 = a2, b39 = b3, a39 = a3, r9 = r, s9 = s, t9 = t as Element of CPS ;
A17: ( o on C2 & b2 on C2 ) by A3, INCSP_1:2;
A18: s on B3 by A10, INCSP_1:2;
 ( b2 on B3 & b1 on B3 ) by A10, INCSP_1:2;
then A19: b19,b29,s9 is_collinear by A18, Th10;
A20: r on B2 by A9, INCSP_1:2;
 ( b3 on B2 & b1 on B2 ) by A9, INCSP_1:2;
then A21: b19,b39,r9 is_collinear by A20, Th10;
A22: t on B1 by A8, INCSP_1:2;
 ( b3 on B1 & b2 on B1 ) by A8, INCSP_1:2;
then A23: b29,b39,t9 is_collinear by A22, Th10;
A24: s on A3 by A7, INCSP_1:2;
 ( a2 on A3 & a1 on A3 ) by A7, INCSP_1:2;
then A25: a19,a29,s9 is_collinear by A24, Th10;
A26: ( o on C3 & b3 on C3 ) by A4, INCSP_1:2;
 a3 on C3 by A4, INCSP_1:2;
then A27: o9,b39,a39 is_collinear by A26, Th10;
 a2 on C2 by A3, INCSP_1:2;
then A28: o9,b29,a29 is_collinear by A17, Th10;
A29: r on A2 by A6, INCSP_1:2;
 ( a3 on A2 & a1 on A2 ) by A6, INCSP_1:2;
then A30: a19,a39,r9 is_collinear by A29, Th10;
A31: t on A1 by A5, INCSP_1:2;
 ( a3 on A1 & a2 on A1 ) by A5, INCSP_1:2;
then A32: a29,a39,t9 is_collinear by A31, Th10;
A33: ( o on C1 & b1 on C1 ) by A2, INCSP_1:2;
A34: ( not o9,b19,b29 is_collinear & not o9,b19,b39 is_collinear & not o9,b29,b39 is_collinear )
proof
A35: now__::_thesis:_not_o9,b19,b39_is_collinear
assume  o9,b19,b39 is_collinear ; ::_thesis: contradiction
then consider K being LINE of (IncProjSp_of CPS) such that
A36: ( o on K & b1 on K & b3 on K ) by Th10;
 ( K = C1 & K = C3 ) by A13, A15, A33, A26, A36, Th8;
hence  contradiction by A11, ZFMISC_1:def_5; ::_thesis: verum
end;
A37: now__::_thesis:_not_o9,b19,b29_is_collinear
assume  o9,b19,b29 is_collinear ; ::_thesis: contradiction
then consider K being LINE of (IncProjSp_of CPS) such that
A38: ( o on K & b1 on K & b2 on K ) by Th10;
 ( K = C1 & K = C2 ) by A13, A14, A33, A17, A38, Th8;
hence  contradiction by A11, ZFMISC_1:def_5; ::_thesis: verum
end;
A39: now__::_thesis:_not_o9,b29,b39_is_collinear
assume  o9,b29,b39 is_collinear ; ::_thesis: contradiction
then consider K being LINE of (IncProjSp_of CPS) such that
A40: ( o on K & b2 on K & b3 on K ) by Th10;
 ( K = C2 & K = C3 ) by A14, A15, A17, A26, A40, Th8;
hence  contradiction by A11, ZFMISC_1:def_5; ::_thesis: verum
end;
assume  ( o9,b19,b29 is_collinear or o9,b19,b39 is_collinear or o9,b29,b39 is_collinear ) ; ::_thesis: contradiction
hence  contradiction by A37, A35, A39; ::_thesis: verum
end;
 a1 on C1 by A2, INCSP_1:2;
then  o9,b19,a19 is_collinear by A33, Th10;
then  t9,r9,s9 is_collinear by A1, A12, A16, A19, A25, A21, A30, A23, A32, A28, A27, A34;
then consider O being LINE of (IncProjSp_of CPS) such that
A41: ( t on O & r on O & s on O ) by Th10;
 {r,s,t} on O by A41, INCSP_1:2;
hence  ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O ; ::_thesis: verum
end;

theorem Th19: :: INCPROJ:19
for CPS being CollProjectiveSpace st ( for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear ) holds
for o, a1, a2, a3, b1, b2, b3, c1, c2, c3 being POINT of (IncProjSp_of CPS)
for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of (IncProjSp_of CPS) st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3
proof
let CPS be CollProjectiveSpace; ::_thesis: ( ( for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear ) implies for o, a1, a2, a3, b1, b2, b3, c1, c2, c3 being POINT of (IncProjSp_of CPS)
for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of (IncProjSp_of CPS) st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3 )
assume A1: for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear ; ::_thesis: for o, a1, a2, a3, b1, b2, b3, c1, c2, c3 being POINT of (IncProjSp_of CPS)
for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of (IncProjSp_of CPS) st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3
let o, a1, a2, a3, b1, b2, b3, c1, c2, c3 be POINT of (IncProjSp_of CPS); ::_thesis: for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of (IncProjSp_of CPS) st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3
let A1, A2, A3, B1, B2, B3, C1, C2, C3 be LINE of (IncProjSp_of CPS); ::_thesis: ( o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 implies c3 on C3 )
assume that
A2: o,a1,a2,a3 are_mutually_different and
A3: o,b1,b2,b3 are_mutually_different and
A4: A3 <> B3 and
A5: o on A3 and
A6: o on B3 and
A7: {a2,b3,c1} on A1 and
A8: {a3,b1,c2} on B1 and
A9: {a1,b2,c3} on C1 and
A10: {a1,b3,c2} on A2 and
A11: {a3,b2,c1} on B2 and
A12: {a2,b1,c3} on C2 and
A13: {b1,b2,b3} on A3 and
A14: {a1,a2,a3} on B3 and
A15: {c1,c2} on C3 ; ::_thesis: c3 on C3
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3, c19 = c1, c29 = c2, c39 = c3 as Point of CPS ;
A16: b1 on A3 by A13, INCSP_1:2;
A17: c3 on C1 by A9, INCSP_1:2;
 ( a1 on C1 & b2 on C1 ) by A9, INCSP_1:2;
then A18: a19,b29,c39 is_collinear by A17, Th10;
A19: c1 on A1 by A7, INCSP_1:2;
A20: ( o9 <> b39 & b29 <> b39 ) by A3, ZFMISC_1:def_6;
A21: ( a29 <> a39 & a19 <> a29 ) by A2, ZFMISC_1:def_6;
A22: ( b3 on A2 & c2 on A2 ) by A10, INCSP_1:2;
A23: a1 on A2 by A10, INCSP_1:2;
then A24: a19,b39,c29 is_collinear by A22, Th10;
A25: ( b19 <> b29 & b19 <> b39 ) by A3, ZFMISC_1:def_6;
A26: b3 on A1 by A7, INCSP_1:2;
A27: a1 on B3 by A14, INCSP_1:2;
A28: not o9,a19,b19 is_collinear
proof
A29: o <> a1 by A2, ZFMISC_1:def_6;
assume  o9,a19,b19 is_collinear ; ::_thesis: contradiction
then consider K being LINE of (IncProjSp_of CPS) such that
A30: o on K and
A31: a1 on K and
A32: b1 on K by Th10;
 o <> b1 by A3, ZFMISC_1:def_6;
then  K = A3 by A5, A16, A30, A32, Th8;
hence  contradiction by A4, A6, A27, A30, A31, A29, Th8; ::_thesis: verum
end;
A33: c3 on C2 by A12, INCSP_1:2;
 ( a2 on C2 & b1 on C2 ) by A12, INCSP_1:2;
then A34: b19,a29,c39 is_collinear by A33, Th10;
A35: a3 on B1 by A8, INCSP_1:2;
A36: b2 on A3 by A13, INCSP_1:2;
then A37: o9,b19,b29 is_collinear by A5, A16, Th10;
A38: ( a3 on B2 & c1 on B2 ) by A11, INCSP_1:2;
A39: b2 on B2 by A11, INCSP_1:2;
then A40: a39,b29,c19 is_collinear by A38, Th10;
A41: b3 on A3 by A13, INCSP_1:2;
then A42: o9,b19,b39 is_collinear by A5, A16, Th10;
A43: ( a19 <> a39 & o9 <> b29 ) by A2, A3, ZFMISC_1:def_6;
A44: ( o9 <> a29 & o9 <> a39 ) by A2, ZFMISC_1:def_6;
A45: c2 on B1 by A8, INCSP_1:2;
A46: a2 on A1 by A7, INCSP_1:2;
then A47: a29,b39,c19 is_collinear by A26, A19, Th10;
A48: b1 <> b2 by A3, ZFMISC_1:def_6;
A49: a1 <> a2 by A2, ZFMISC_1:def_6;
A50: o <> b3 by A3, ZFMISC_1:def_6;
A51: b1 on B1 by A8, INCSP_1:2;
then A52: a39,b19,c29 is_collinear by A35, A45, Th10;
A53: a3 on B3 by A14, INCSP_1:2;
then A54: o9,a19,a39 is_collinear by A6, A27, Th10;
A55: a2 on B3 by A14, INCSP_1:2;
then  o9,a19,a29 is_collinear by A6, A27, Th10;
then  c19,c29,c39 is_collinear by A1, A44, A21, A43, A20, A25, A28, A54, A37, A42, A18, A34, A24, A52, A47, A40;
then A56: ex K being LINE of (IncProjSp_of CPS) st
( c1 on K & c2 on K & c3 on K ) by Th10;
A57: o <> a3 by A2, ZFMISC_1:def_6;
A58: c1 <> c2
proof
assume A59: not c1 <> c2 ; ::_thesis: contradiction
 not a3 on A3 by A4, A5, A6, A57, A53, Th8;
then  B1 <> B2 by A48, A35, A51, A39, A16, A36, Th8;
then A60: c1 = a3 by A35, A45, A38, A59, Th8;
 not b3 on B3 by A4, A5, A6, A50, A41, Th8;
then  A1 <> A2 by A49, A46, A26, A23, A27, A55, Th8;
then  c1 = b3 by A26, A19, A22, A59, Th8;
hence  contradiction by A4, A5, A6, A50, A41, A53, A60, Th8; ::_thesis: verum
end;
 ( c1 on C3 & c2 on C3 ) by A15, INCSP_1:1;
hence  c3 on C3 by A58, A56, Th8; ::_thesis: verum
end;

definition
let S be IncProjStr ;
attrS is partial  means :Def4: :: INCPROJ:def 4
 for p, q being POINT of S
for P, Q being LINE of S st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q;
redefine attr S is linear  means :Def5: :: INCPROJ:def 5
 for p, q being POINT of S ex P being LINE of S st
( p on P & q on P );
compatibility
 ( S is linear iff for p, q being POINT of S ex P being LINE of S st
( p on P & q on P ) )
proof
hereby  ::_thesis: ( ( for p, q being POINT of S ex P being LINE of S st
( p on P & q on P ) ) implies S is linear )
assume A1: S is linear ; ::_thesis: for p, q being POINT of S ex P being LINE of S st
( p on P & q on P )
let p, q be POINT of S; ::_thesis: ex P being LINE of S st
( p on P & q on P )
consider P being LINE of S such that
A2: {p,q} on P by A1, INCSP_1:def_9;
take P = P; ::_thesis: ( p on P & q on P )
thus  ( p on P & q on P ) by A2, INCSP_1:1; ::_thesis: verum
end;
assume A3: for p, q being POINT of S ex P being LINE of S st
( p on P & q on P ) ; ::_thesis: S is linear
let p, q be POINT of S; :: according to INCSP_1:def_9 ::_thesis: ex b1 being Element of the Lines of S st {p,q} on b1
consider L being LINE of S such that
A4: ( p on L & q on L ) by A3;
 {p,q} on L by A4, INCSP_1:1;
hence  ex b1 being Element of the Lines of S st {p,q} on b1 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines partial INCPROJ:def_4_:_
 for S being IncProjStr holds
( S is partial iff for p, q being POINT of S
for P, Q being LINE of S st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q );

:: deftheorem Def5 defines linear INCPROJ:def_5_:_
 for S being IncProjStr holds
( S is linear iff for p, q being POINT of S ex P being LINE of S st
( p on P & q on P ) );

definition
let S be IncProjStr ;
attrS is up-2-dimensional  means :Def6: :: INCPROJ:def 6
 not for p being POINT of S
for P being LINE of S holds p on P;
attrS is up-3-rank  means :Def7: :: INCPROJ:def 7
 for P being LINE of S ex a, b, c being POINT of S st
( a <> b & b <> c & c <> a & a on P & b on P & c on P );
attrS is Vebleian  means :Def8: :: INCPROJ:def 8
 for a, b, c, d, p, q being POINT of S
for M, N, P, Q being LINE of S st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of S st
( q on P & q on Q );
end;

:: deftheorem Def6 defines up-2-dimensional INCPROJ:def_6_:_
 for S being IncProjStr holds
( S is up-2-dimensional iff not for p being POINT of S
for P being LINE of S holds p on P );

:: deftheorem Def7 defines up-3-rank INCPROJ:def_7_:_
 for S being IncProjStr holds
( S is up-3-rank iff for P being LINE of S ex a, b, c being POINT of S st
( a <> b & b <> c & c <> a & a on P & b on P & c on P ) );

:: deftheorem Def8 defines Vebleian INCPROJ:def_8_:_
 for S being IncProjStr holds
( S is Vebleian iff for a, b, c, d, p, q being POINT of S
for M, N, P, Q being LINE of S st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of S st
( q on P & q on Q ) );

registration
let CPS be CollProjectiveSpace;
cluster IncProjSp_of CPS ->  linear partial up-2-dimensional up-3-rank Vebleian ;
coherence
 ( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian )
proof
set PS = IncProjSp_of CPS;
A1: for a, b, c, d, p, q being POINT of (IncProjSp_of CPS)
for M, N, P, Q being LINE of (IncProjSp_of CPS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q ) by Th13;
A2: ( not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P & ( for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P ) ) ) by Th11, Th12;
 ( ( for p, q being POINT of (IncProjSp_of CPS)
for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q ) & ( for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) ) ) by Th8, Th9;
hence  ( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian ) by A2, A1, Def4, Def5, Def6, Def7, Def8; ::_thesis: verum
end;
end;

registration
cluster strict linear partial up-2-dimensional up-3-rank Vebleian for 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
set CPS = the CollProjectiveSpace;
 ( IncProjSp_of the CollProjectiveSpace is strict & IncProjSp_of the CollProjectiveSpace is partial & IncProjSp_of the CollProjectiveSpace is linear & IncProjSp_of the CollProjectiveSpace is up-2-dimensional & IncProjSp_of the CollProjectiveSpace is up-3-rank & IncProjSp_of the CollProjectiveSpace is Vebleian ) ;
hence  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 ) ; ::_thesis: verum
end;
end;

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

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

definition
let IT be IncProjSp;
attrIT is 2-dimensional  means :Def9: :: INCPROJ:def 9
 for M, N being LINE of IT ex q being POINT of IT st
( q on M & q on N );
end;

:: deftheorem Def9 defines 2-dimensional INCPROJ:def_9_:_
 for IT being IncProjSp holds
( IT is 2-dimensional iff for M, N being LINE of IT ex q being POINT of IT st
( q on M & q on N ) );

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

definition
let IT be IncProjStr ;
attrIT is at_most-3-dimensional  means :Def10: :: INCPROJ:def 10
 for a being POINT of IT
for M, N being LINE of IT ex b, c being POINT of IT ex S being LINE of IT st
( a on S & b on S & c on S & b on M & c on N );
end;

:: deftheorem Def10 defines at_most-3-dimensional INCPROJ:def_10_:_
 for IT being IncProjStr holds
( IT is at_most-3-dimensional iff for a being POINT of IT
for M, N being LINE of IT ex b, c being POINT of IT ex S being LINE of IT st
( a on S & b on S & c on S & b on M & c on N ) );

definition
let IT be IncProjSp;
attrIT is 3-dimensional  means :: INCPROJ:def 11
( IT is at_most-3-dimensional & IT is up-3-dimensional );
end;

:: deftheorem  defines 3-dimensional INCPROJ:def_11_:_
 for IT being IncProjSp holds
( IT is 3-dimensional iff ( IT is at_most-3-dimensional & IT is up-3-dimensional ) );

definition
let IT be IncProjStr ;
attrIT is Fanoian  means :Def12: :: INCPROJ:def 12
 for p, q, r, s, a, b, c being POINT of IT
for L, Q, R, S, A, B, C being LINE of IT st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C;
end;

:: deftheorem Def12 defines Fanoian INCPROJ:def_12_:_
 for IT being IncProjStr holds
( IT is Fanoian iff for p, q, r, s, a, b, c being POINT of IT
for L, Q, R, S, A, B, C being LINE of IT st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C );

definition
let IT be IncProjStr ;
attrIT is Desarguesian  means :Def13: :: INCPROJ:def 13
 for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IT
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IT st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of IT st {r,s,t} on O;
end;

:: deftheorem Def13 defines Desarguesian INCPROJ:def_13_:_
 for IT being IncProjStr holds
( IT is Desarguesian iff for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IT
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IT st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of IT st {r,s,t} on O );

definition
let IT be IncProjStr ;
attrIT is Pappian  means :Def14: :: INCPROJ:def 14
 for o, a1, a2, a3, b1, b2, b3, c1, c2, c3 being POINT of IT
for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of IT st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3;
end;

:: deftheorem Def14 defines Pappian INCPROJ:def_14_:_
 for IT being IncProjStr holds
( IT is Pappian iff for o, a1, a2, a3, b1, b2, b3, c1, c2, c3 being POINT of IT
for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of IT st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3 );

registration
cluster linear partial up-2-dimensional up-3-rank Vebleian up-3-dimensional at_most-3-dimensional Fanoian Desarguesian for IncProjStr ;
existence
 ex b1 being IncProjSp st
( b1 is Desarguesian & b1 is Fanoian & b1 is at_most-3-dimensional & b1 is up-3-dimensional )
proof
set CPS = the Fanoian Desarguesian up-3-dimensional at_most-3-dimensional CollProjectiveSpace;
reconsider CPS9 = the Fanoian Desarguesian up-3-dimensional at_most-3-dimensional CollProjectiveSpace as CollProjectiveSpace ;
take X = IncProjSp_of CPS9; ::_thesis: ( X is Desarguesian & X is Fanoian & X is at_most-3-dimensional & X is up-3-dimensional )
 for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS9 st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear by ANPROJ_2:def_12;
then A1: for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of X
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of X st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of X st {r,s,t} on O by Th18;
 ex p, p1, r, r1 being Point of CPS9 st
for s being Point of CPS9 holds
( not p,p1,s is_collinear or not r,r1,s is_collinear ) by ANPROJ_2:def_14;
then A2: ex M, N being LINE of X st
for q being POINT of X holds
( not q on M or not q on N ) by Th15;
 for p, p1, q, q1, r2 being Point of CPS9 ex r, r1 being Point of CPS9 st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) by ANPROJ_2:def_15;
then A3: for a being POINT of X
for M, N being LINE of X ex b, c being POINT of X ex S being LINE of X st
( a on S & b on S & c on S & b on M & c on N ) by Th16;
 for p1, r2, q, r1, q1, p, r being Point of CPS9 st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear by ANPROJ_2:def_11;
then  for p, q, r, s, a, b, c being POINT of X
for L, Q, R, S, A, B, C being LINE of X st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C by Th17;
hence  ( X is Desarguesian & X is Fanoian & X is at_most-3-dimensional & X is up-3-dimensional ) by A1, A2, A3, Def9, Def10, Def12, Def13; ::_thesis: verum
end;
end;

registration
cluster linear partial up-2-dimensional up-3-rank Vebleian up-3-dimensional at_most-3-dimensional Fanoian Pappian for IncProjStr ;
existence
 ex b1 being IncProjSp st
( b1 is Pappian & b1 is Fanoian & b1 is at_most-3-dimensional & b1 is up-3-dimensional )
proof
set CPS = the Fanoian Pappian up-3-dimensional at_most-3-dimensional CollProjectiveSpace;
reconsider CPS9 = the Fanoian Pappian up-3-dimensional at_most-3-dimensional CollProjectiveSpace as CollProjectiveSpace ;
take X = IncProjSp_of CPS9; ::_thesis: ( X is Pappian & X is Fanoian & X is at_most-3-dimensional & X is up-3-dimensional )
 for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS9 st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear by ANPROJ_2:def_13;
then A1: for o, a1, a2, a3, b1, b2, b3, c1, c2, c3 being POINT of X
for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of X st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3 by Th19;
 ex p, p1, r, r1 being Point of CPS9 st
for s being Point of CPS9 holds
( not p,p1,s is_collinear or not r,r1,s is_collinear ) by ANPROJ_2:def_14;
then A2: ex M, N being LINE of X st
for q being POINT of X holds
( not q on M or not q on N ) by Th15;
 for p, p1, q, q1, r2 being Point of CPS9 ex r, r1 being Point of CPS9 st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) by ANPROJ_2:def_15;
then A3: for a being POINT of X
for M, N being LINE of X ex b, c being POINT of X ex S being LINE of X st
( a on S & b on S & c on S & b on M & c on N ) by Th16;
 for p1, r2, q, r1, q1, p, r being Point of CPS9 st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear by ANPROJ_2:def_11;
then  for p, q, r, s, a, b, c being POINT of X
for L, Q, R, S, A, B, C being LINE of X st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C by Th17;
hence  ( X is Pappian & X is Fanoian & X is at_most-3-dimensional & X is up-3-dimensional ) by A1, A2, A3, Def9, Def10, Def12, Def14; ::_thesis: verum
end;
end;

registration
cluster linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional Fanoian Desarguesian for IncProjStr ;
existence
 ex b1 being IncProjSp st
( b1 is Desarguesian & b1 is Fanoian & b1 is 2-dimensional )
proof
set CPS = the Fanoian Desarguesian CollProjectivePlane;
reconsider CPS9 = the Fanoian Desarguesian CollProjectivePlane as CollProjectiveSpace ;
take X = IncProjSp_of CPS9; ::_thesis: ( X is Desarguesian & X is Fanoian & X is 2-dimensional )
 for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS9 st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear by ANPROJ_2:def_12;
then A1: for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of X
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of X st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of X st {r,s,t} on O by Th18;
 for a, b, c, d being Point of CPS9 ex p being Point of CPS9 st
( a,b,p is_collinear & c,d,p is_collinear ) by ANPROJ_2:def_14;
then A2: for M, N being LINE of X ex q being POINT of X st
( q on M & q on N ) by Th14;
 for p1, r2, q, r1, q1, p, r being Point of CPS9 st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear by ANPROJ_2:def_11;
then  for p, q, r, s, a, b, c being POINT of X
for L, Q, R, S, A, B, C being LINE of X st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C by Th17;
hence  ( X is Desarguesian & X is Fanoian & X is 2-dimensional ) by A1, A2, Def9, Def12, Def13; ::_thesis: verum
end;
end;

registration
cluster linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional Fanoian Pappian for IncProjStr ;
existence
 ex b1 being IncProjSp st
( b1 is Pappian & b1 is Fanoian & b1 is 2-dimensional )
proof
set CPS = the Fanoian Pappian CollProjectivePlane;
reconsider CPS9 = the Fanoian Pappian CollProjectivePlane as CollProjectiveSpace ;
take X = IncProjSp_of CPS9; ::_thesis: ( X is Pappian & X is Fanoian & X is 2-dimensional )
 for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of CPS9 st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear by ANPROJ_2:def_13;
then A1: for o, a1, a2, a3, b1, b2, b3, c1, c2, c3 being POINT of X
for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of X st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3 by Th19;
 for a, b, c, d being Point of CPS9 ex p being Point of CPS9 st
( a,b,p is_collinear & c,d,p is_collinear ) by ANPROJ_2:def_14;
then A2: for M, N being LINE of X ex q being POINT of X st
( q on M & q on N ) by Th14;
 for p1, r2, q, r1, q1, p, r being Point of CPS9 st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear by ANPROJ_2:def_11;
then  for p, q, r, s, a, b, c being POINT of X
for L, Q, R, S, A, B, C being LINE of X st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C by Th17;
hence  ( X is Pappian & X is Fanoian & X is 2-dimensional ) by A1, A2, Def9, Def12, Def14; ::_thesis: verum
end;
end;