let IPP be IncProjSp; :: thesis: for A, B being LINE of IPP ex a being POINT of IPP st
( not a on A & not a on B )
let A, B be LINE of IPP; :: thesis: ex a being POINT of IPP st
( not a on A & not a on B )
A1: ( A = B implies ex a being POINT of IPP st
( not a on A & not a on B ) )

proof

assume A2: A = B ; :: thesis: ex a being POINT of IPP st
( not a on A & not a on B )
not for a being POINT of IPP holds a on A by Th1;
hence ex a being POINT of IPP st
( not a on A & not a on B ) by A2; :: thesis: verum

end;

( A <> B implies ex a being POINT of IPP st
( not a on A & not a on B ) )

proof

assume A <> B ; :: thesis: ex a being POINT of IPP st
( not a on A & not a on B )
then consider a, b being POINT of IPP such that
A3: ( a on A & not a on B & b on B & not b on A ) by Th3;
consider C being LINE of IPP such that
A4: ( a on C & b on C ) by INCPROJ:def 10;
consider c, d, e being Element of the Points of IPP such that
A5: ( c <> d & d <> e & e <> c & c on C & d on C & e on C ) by INCPROJ:def 12;
( ( not c on A & not c on B ) or ( not d on A & not d on B ) or ( not e on A & not e on B ) ) by A3, A4, A5, INCPROJ:def 9;
hence ex a being POINT of IPP st
( not a on A & not a on B ) ; :: thesis: verum

end;

hence ex a being POINT of IPP st
( not a on A & not a on B ) by A1; :: thesis: verum