let IPP be Fanoian IncProjSp; :: thesis: for B being LINE of ex p, q, r, s being POINT of st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
let B be LINE of ; :: thesis: ex p, q, r, s being POINT of st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
ex a, b, c, d being POINT of ex A being LINE of st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) by Th18;
hence ex p, q, r, s being POINT of st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by Th15; :: thesis: verum