theorem Th12:
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