let IPP be IncProjSp; :: thesis: for a, b being POINT of IPP
for A being LINE of IPP ex c being POINT of IPP st
( c on A & c <> a & c <> b )
let a, b be POINT of IPP; :: thesis: for A being LINE of IPP ex c being POINT of IPP st
( c on A & c <> a & c <> b )
let A be LINE of IPP; :: thesis: ex c being POINT of IPP st
( c on A & c <> a & c <> b )
consider p, q, r being POINT of IPP such that
A1: ( p <> q & q <> r & r <> p ) and
A2: ( p on A & q on A & r on A ) by INCPROJ:def 7;
( ( p <> a & p <> b ) or ( q <> a & q <> b ) or ( r <> a & r <> b ) ) by A1;
hence ex c being POINT of IPP st
( c on A & c <> a & c <> b ) by A2; :: thesis: verum