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 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds
r1,r2,r3 are_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_distinct & 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 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 Desarguesian & X is Fanoian & X is at_most-3-dimensional & X is up-3-dimensional ) by A1, A2, A3; :: thesis: verum