let IPP be IncProjSp; :: thesis: for a, b being POINT of IPP ex A being LINE of IPP st
( not a on A & not b on A )
let a, b be POINT of IPP; :: thesis: ex A being LINE of IPP st
( not a on A & not b on A )
now :: thesis: ex A being LINE of IPP st
( not a on A & not b on A )
consider A being LINE of IPP such that
A1: ( a on A & b on A ) by INCPROJ:def 5;
consider c being POINT of IPP such that
A2: ( c on A & c <> a & c <> b ) by Th8;
consider d being POINT of IPP such that
A3: not d on A by Th1;
consider B being LINE of IPP such that
A4: ( d on B & c on B ) by INCPROJ:def 5;
( not a on B & not b on B ) by A1, A2, A3, A4, INCPROJ:def 4;
hence ex A being LINE of IPP st
( not a on A & not b on A ) ; :: thesis: verum
end;
hence ex A being LINE of IPP st
( not a on A & not b on A ) ; :: thesis: verum