let IPP be Fanoian IncProjSp; :: thesis: 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; :: thesis: 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; :: thesis: verum