let IPP be IncProjSp; :: thesis: for a being POINT of IPP ex A, B, C being LINE of IPP st
( a on A & a on B & a on C & A <> B & B <> C & C <> A )
let a be POINT of IPP; :: thesis: ex A, B, C being LINE of IPP st
( a on A & a on B & a on C & A <> B & B <> C & C <> A )
consider Q being LINE of IPP such that
A1: not a on Q by Th2;
consider b1, b2, b3 being Element of the Points of IPP such that
A2: ( b1 <> b2 & b2 <> b3 & b3 <> b1 & b1 on Q & b2 on Q & b3 on Q ) by INCPROJ:def 12;
consider B1 being LINE of IPP such that
A3: ( a on B1 & b1 on B1 ) by INCPROJ:def 10;
consider B2 being LINE of IPP such that
A4: ( a on B2 & b2 on B2 ) by INCPROJ:def 10;
consider B3 being Element of the Lines of IPP such that
A5: ( a on B3 & b3 on B3 ) by INCPROJ:def 10;
A6: not b1 on B2 by A1, A2, A4, INCPROJ:def 9;
A7: not b2 on B3 by A1, A2, A5, INCPROJ:def 9;
not b3 on B1 by A1, A2, A3, INCPROJ:def 9;
hence ex A, B, C being LINE of IPP st
( a on A & a on B & a on C & A <> B & B <> C & C <> A ) by A3, A4, A5, A6, A7; :: thesis: verum