let IPP be Fanoian IncProjSp; ex a being POINT of IPP ex A, B, C, D being LINE of IPP st
( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_distinct )
consider p, q, r, s, a, b, c being POINT of IPP, A, B, C, Q, L, R, S, D being LINE of IPP, d being POINT of IPP such that
not q on L
and
not r on L
and
not p on Q
and
not s on Q
and
not p on R
and
not r on R
and
not q on S
and
not s on S
and
{a,p,s} on L
and
{a,q,r} on Q
and
A1:
( {b,q,s} on R & {b,p,r} on S )
and
{c,p,q} on A
and
{c,r,s} on B
and
A2:
{a,b} on C
and
not c on C
and
A3:
b on D
and
c on D
and
A4:
C,D,R,S are_mutually_distinct
and
d on A
and
c,d,p,q are_mutually_distinct
by Lm2;
A5:
b on C
by A2, INCSP_1:1;
( b on S & b on R )
by A1, INCSP_1:2;
hence
ex a being POINT of IPP ex A, B, C, D being LINE of IPP st
( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_distinct )
by A3, A4, A5; verum