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 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 ) 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_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