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

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

assume A,B,C are_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 TOPREAL9:67;

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 A2: B in Line (C,A) by Th12;
A3: ( C in Line (C,A) & A in Line (C,A) ) by EUCLID_4:41;
then Line (C,A) c= Line (B,C) by A2, A1, EUCLID_4:43;
hence A in Line (B,C) by A3; :: thesis: verum

end;

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

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

end;

end;

end;

assume A in Line (B,C) ; :: thesis: A,B,C are_collinear
then consider lambda being Real such that
A6: 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, A6;
hence A,B,C are_collinear by Th9; :: thesis: verum