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

hereby :: thesis:

assume A,B,C are_collinear ; :: thesis:

per cases by TOPREAL9:67;

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

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

end;

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

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:

end;

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

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:

end;

end;

end;

assume A in Line (B,C) ; :: thesis:
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: