let IPP be IncProjSp; ( 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 )
; 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 )
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; verum