let IPP be IncProjSp; for a, b being POINT of IPP st a <> b holds
ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A )
let a, b be POINT of IPP; ( a <> b implies ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A ) )
consider Q being LINE of IPP such that
A1:
( a on Q & b on Q )
by INCPROJ:def 5;
consider q being POINT of IPP such that
A2:
not q on Q
by Th1;
consider B being LINE of IPP such that
A3:
b on B
and
A4:
q on B
by INCPROJ:def 5;
assume A5:
a <> b
; ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A )
then A6:
not a on B
by A1, A2, A3, A4, INCPROJ:def 4;
consider A being LINE of IPP such that
A7:
a on A
and
A8:
q on A
by INCPROJ:def 5;
not b on A
by A5, A1, A2, A7, A8, INCPROJ:def 4;
hence
ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A )
by A7, A3, A6; verum