let IPP be IncProjSp; for A, B being LINE of IPP st A <> B holds
ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )
let A, B be LINE of IPP; ( A <> B implies ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A ) )
consider a, b, d being POINT of IPP such that
A1:
a <> b
and
b <> d
and
d <> a
and
A2:
( a on A & b on A )
and
d on A
by INCPROJ:def 7;
consider r, s, t being POINT of IPP such that
A3:
r <> s
and
s <> t
and
t <> r
and
A4:
( r on B & s on B )
and
t on B
by INCPROJ:def 7;
assume A5:
A <> B
; ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )
then A6:
( not r on A or not s on A )
by A3, A4, INCPROJ:def 4;
( not a on B or not b on B )
by A5, A1, A2, INCPROJ:def 4;
hence
ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )
by A2, A4, A6; verum