let IPP be IncProjSp; :: thesis: for A, B being LINE of IPP st A <> B holds
ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )
let A, B be LINE of IPP; :: thesis: ( A <> B implies ex a, b being POINT 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 POINT of IPP st
( a on A & not a on B & b on B & not b on A )
consider a, b, d being POINT of IPP such that
A2: ( a <> b & b <> d & d <> a & a on A & b on A & d on A ) by INCPROJ:def 12;
consider r, s, t being POINT of IPP such that
A3: ( r <> s & s <> t & t <> r & r on B & s on B & t on B ) by INCPROJ:def 12;
A4: ( not a on B or not b on B ) by A1, A2, INCPROJ:def 9;
( not r on A or not s on A ) by A1, A3, INCPROJ:def 9;
hence ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A ) by A2, A3, A4; :: thesis: verum