for IPP being Desarguesian IncProjSp
for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IPP
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP 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 <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds
ex O being LINE of IPP st {r,s,t} on O