let IPP be IncProjSp; 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; 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 ) )
( A = B implies ex a being POINT of IPP st
( not a on A & not a on B ) )
proof
assume A6:
A = B
;
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;
verum
end;
hence
ex a being POINT of IPP st
( not a on A & not a on B )
by A1; verum