let IPP be Fanoian IncProjSp; for B being LINE of IPP ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )
let B be LINE of IPP; ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )
ex a, b, c, d being POINT of IPP ex A being LINE of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct )
by Th16;
hence
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )
by Th13; verum