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 is_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 is_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 is_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 is_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 is_collinear )

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

A5: now

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 Th2;
a9 in Line a9,b9 by COLLSP:16;
then A6: a on P by A1, Th9;
b9 in Line a9,b9 by COLLSP:16;
then A7: b on P by A2, Th9;
c9 in Line a9,b9 by A4, COLLSP:17;
then c on P by A3, Th9;
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

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 Th13;
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 is_collinear
reconsider P9 = P as LINE of CPS by Th2;
A11: c9 in P9 by A3, A10, Th9;
( a9 in P9 & b9 in P9 ) by A1, A2, A9, Th9;
hence a9,b9,c9 is_collinear by A11, COLLSP:25; :: thesis: verum