let IPP be IncProjSp; :: thesis: 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; :: thesis: ( 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 ) )
assume A1: a <> b ; :: thesis: 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
A2: ( a on Q & b on Q ) by INCPROJ:def 10;
consider q being POINT of IPP such that
A3: not q on Q by Th1;
consider A being LINE of IPP such that
A4: ( a on A & q on A ) by INCPROJ:def 10;
consider B being LINE of IPP such that
A5: ( b on B & q on B ) by INCPROJ:def 10;
A6: not b on A by A1, A2, A3, A4, INCPROJ:def 9;
not a on B by A1, A2, A3, A5, INCPROJ:def 9;
hence ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A ) by A4, A5, A6; :: thesis: verum