let CPS be proper CollSp; :: thesis: for a, b, c being POINT of (IncProjSp_of CPS)
for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
let a, b, c be POINT of (IncProjSp_of CPS); :: thesis: for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
let a9, b9, c9 be Point of CPS; :: thesis: ( a = a9 & b = b9 & c = c9 implies ( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) ) )
assume that
A1: a = a9 and
A2: b = b9 and
A3: c = c9 ; :: thesis: ( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )

hereby :: thesis: ( ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) implies a9,b9,c9 are_collinear )

assume A4: a9,b9,c9 are_collinear ; :: thesis: ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )

A5: now :: thesis: ( a9 <> b9 implies ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )

set X = Line (a9,b9);
assume a9 <> b9 ; :: thesis: ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )
then reconsider P9 = Line (a9,b9) as LINE of CPS by COLLSP:def 7;
reconsider P = P9 as LINE of (IncProjSp_of CPS) by Th1;
a9 in Line (a9,b9) by COLLSP:10;
then A6: a on P by A1, Th5;
b9 in Line (a9,b9) by COLLSP:10;
then A7: b on P by A2, Th5;
c9 in Line (a9,b9) by A4, COLLSP:11;
then c on P by A3, Th5;
hence ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) by A6, A7; :: thesis: verum

end;

now :: thesis: ( a9 = b9 implies ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )

assume A8: a9 = b9 ; :: thesis: ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )
ex P being LINE of (IncProjSp_of CPS) st
( b on P & c on P ) by Th9;
hence ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) by A1, A2, A8; :: thesis: verum

end;

hence ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) by A5; :: thesis: verum

end;

given P being LINE of (IncProjSp_of CPS) such that A9: ( a on P & b on P ) and
A10: c on P ; :: thesis: a9,b9,c9 are_collinear
reconsider P9 = P as LINE of CPS by Th1;
A11: c9 in P9 by A3, A10, Th5;
( a9 in P9 & b9 in P9 ) by A1, A2, A9, Th5;
hence a9,b9,c9 are_collinear by A11, COLLSP:16; :: thesis: verum