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 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
a on A and
A2: not a on B and
b on B and
A3: not b on A by Th3;
consider C being LINE of IPP such that
A4: ( a on C & b on C ) by INCPROJ:def 5;
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 7;
( ( 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 A2, A3, A4, A5, INCPROJ:def 4;
hence ex a being POINT of IPP st
( not a on A & not a on B ) ; :: thesis: verum
end;
( A = B implies ex a being POINT of IPP st
( not a on A & not a on B ) )
proof
assume A6: 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 A6; :: thesis: verum
end;
hence ex a being POINT of IPP st
( not a on A & not a on B ) by A1; :: thesis: verum