let IPP be IncProjSp; :: thesis: ( ex A being LINE of IPP ex a, b, c, d being POINT of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct ) implies 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 ) )
given A being LINE of IPP, a, b, c, d being POINT of IPP such that A1: ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct ) ; :: 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 )
consider x being POINT of IPP such that
A2: x on A by Th7;
consider y being POINT of IPP such that
A3: y on B by Th7;
consider C being LINE of IPP such that
A4: x on C and
A5: y on C by INCPROJ:def 5;
ex p1, q1, r1, s1 being POINT of IPP st
( p1 on C & q1 on C & r1 on C & s1 on C & p1,q1,r1,s1 are_mutually_distinct ) by A1, A2, A4, Lm1;
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 A3, A5, Lm1; :: thesis: verum