let IPP be IncProjSp; 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; 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
and
A3:
b2 <> b3
and
A4:
b3 <> b1
and
A5:
b1 on Q
and
A6:
b2 on Q
and
A7:
b3 on Q
by INCPROJ:def 7;
consider B1 being LINE of IPP such that
A8:
( a on B1 & b1 on B1 )
by INCPROJ:def 5;
A9:
not b3 on B1
by A1, A4, A5, A7, A8, INCPROJ:def 4;
consider B2 being LINE of IPP such that
A10:
( a on B2 & b2 on B2 )
by INCPROJ:def 5;
consider B3 being Element of the Lines of IPP such that
A11:
( a on B3 & b3 on B3 )
by INCPROJ:def 5;
A12:
not b2 on B3
by A1, A3, A6, A7, A11, INCPROJ:def 4;
not b1 on B2
by A1, A2, A5, A6, A10, INCPROJ:def 4;
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 A8, A10, A11, A12, A9; verum