let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ( A,C,B is_a_triangle & B,A,C is_a_triangle & B,C,A is_a_triangle & C,A,B is_a_triangle & C,B,A is_a_triangle ) )
assume A,B,C is_a_triangle ; :: thesis: ( A,C,B is_a_triangle & B,A,C is_a_triangle & B,C,A is_a_triangle & C,A,B is_a_triangle & C,B,A is_a_triangle )
then A: the_area_of_polygon3 (A,B,C) <> 0 by Th9;
then the_area_of_polygon3 (A,C,B) <> 0 ;
hence A,C,B is_a_triangle by Th9; :: thesis: ( B,A,C is_a_triangle & B,C,A is_a_triangle & C,A,B is_a_triangle & C,B,A is_a_triangle )
the_area_of_polygon3 (B,A,C) <> 0 by A;
hence B,A,C is_a_triangle by Th9; :: thesis: ( B,C,A is_a_triangle & C,A,B is_a_triangle & C,B,A is_a_triangle )
the_area_of_polygon3 (B,C,A) <> 0 by A;
hence B,C,A is_a_triangle by Th9; :: thesis: ( C,A,B is_a_triangle & C,B,A is_a_triangle )
the_area_of_polygon3 (C,A,B) <> 0 by A;
hence C,A,B is_a_triangle by Th9; :: thesis: C,B,A is_a_triangle
the_area_of_polygon3 (C,B,A) <> 0 by A;
hence C,B,A is_a_triangle by Th9; :: thesis: verum