theorem
for
IPP being
Fanoian IncProjSp ex
p,
q,
r,
s,
a,
b,
c being
POINT of
IPP ex
A,
B,
C,
Q,
L,
R,
S,
D being
LINE of
IPP 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 & not
c on C )