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

hereby :: thesis: ( ex P being LINE of st
( a on P & b on P & c on P ) implies a',b',c' is_collinear )

assume A4: a',b',c' is_collinear ; :: thesis: ex P being LINE of st
( a on P & b on P & c on P )

A5: now

set X = Line a',b';
assume a' <> b' ; :: thesis: ex P being LINE of st
( a on P & b on P & c on P )
then reconsider P' = Line a',b' as LINE of CPS by COLLSP:def 7;
reconsider P = P' as LINE of by Th2;
a' in Line a',b' by COLLSP:16;
then A6: a on P by A1, Th9;
b' in Line a',b' by COLLSP:16;
then A7: b on P by A2, Th9;
c' in Line a',b' by A4, COLLSP:17;
then c on P by A3, Th9;
hence ex P being LINE of st
( a on P & b on P & c on P ) by A6, A7; :: thesis: verum

end;

now

assume A8: a' = b' ; :: thesis: ex P being LINE of st
( a on P & b on P & c on P )
ex P being LINE of st
( b on P & c on P ) by Th13;
hence ex P being LINE of st
( a on P & b on P & c on P ) by A1, A2, A8; :: thesis: verum

end;

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

end;

given P being LINE of such that A9: ( a on P & b on P ) and
A10: c on P ; :: thesis: a',b',c' is_collinear
reconsider P' = P as LINE of CPS by Th2;
A11: c' in P' by A3, A10, Th9;
( a' in P' & b' in P' ) by A1, A2, A9, Th9;
hence a',b',c' is_collinear by A11, COLLSP:25; :: thesis: verum