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