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 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds
r1,r2,r3 are_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_distinct & o,b1,b2,b3 are_mutually_distinct & 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 are_collinear or not r,r1,s are_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 are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_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 are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds
r2,r1,q1 are_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; :: thesis: verum