let B, C, A be Point of (TOP-REAL 2); :: thesis: ( B <> C implies ( A,B,C is_collinear iff A in Line (B,C) ) )
assume A: B <> C ; :: thesis: ( A,B,C is_collinear iff A in Line (B,C) )

hereby :: thesis: ( A in Line (B,C) implies A,B,C is_collinear )

assume A,B,C is_collinear ; :: thesis: A in Line (B,C)

per cases then ( A in LSeg (B,C) or B in LSeg (C,A) or C in LSeg (A,B) ) by EUCLID_6:def 3;

suppose A in LSeg (B,C) ; :: thesis: A in Line (B,C)

hence A in Line (B,C) by Th12; :: thesis: verum

end;

suppose B in LSeg (C,A) ; :: thesis: A in Line (B,C)

then B: B in Line (C,A) by Th12;
C: ( C in Line (C,A) & A in Line (C,A) ) by EUCLID_4:41;
then Line (C,A) c= Line (B,C) by EUCLID_4:43, B, A;
hence A in Line (B,C) by C; :: thesis: verum

end;

suppose C in LSeg (A,B) ; :: thesis: A in Line (B,C)

then B: C in Line (A,B) by Th12;
C: ( A in Line (A,B) & B in Line (A,B) ) by EUCLID_4:41;
then Line (A,B) c= Line (B,C) by EUCLID_4:43, B, A;
hence A in Line (B,C) by C; :: thesis: verum

end;

end;

end;

assume A in Line (B,C) ; :: thesis: A,B,C is_collinear
then consider lambda being Real such that
A: A = ((1 - lambda) * B) + (lambda * C) ;
the_area_of_polygon3 (A,B,C) = ((1 - lambda) * (the_area_of_polygon3 (B,B,C))) + (lambda * (the_area_of_polygon3 (C,B,C))) by Th7, A;
hence A,B,C is_collinear by Th9; :: thesis: verum