let IPP be Fanoian IncProjSp; :: thesis: 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_different )
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 & 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 ) and
A1: ( {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 ) and
not c on C and
A2: ( b on D & c on D & C,D,R,S are_mutually_different ) and
( d on A & c,d,p,q are_mutually_different ) by Lm2;
( b on S & b on R & b on C ) by A1, INCSP_1:11, INCSP_1:12;
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_different ) by A2; :: thesis: verum