let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ( |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B))) & |.(B - C).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (B,A,C))) & |.(C - A).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A))) ) )
assume A1: A,B,C is_a_triangle ; :: thesis: ( |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B))) & |.(B - C).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (B,A,C))) & |.(C - A).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A))) )
then A2: ( B,C,A is_a_triangle & C,A,B is_a_triangle ) by MENELAUS:15;
A3: |.(B - C).| = (the_diameter_of_the_circumcircle (B,C,A)) * (sin (angle (B,A,C))) by A2, Lm10;
thus |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B))) by A1, Lm10; :: thesis: ( |.(B - C).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (B,A,C))) & |.(C - A).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A))) )
thus |.(B - C).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (B,A,C))) by A3, Thm27; :: thesis: |.(C - A).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A)))
|.(C - A).| = (the_diameter_of_the_circumcircle (C,A,B)) * (sin (angle (C,B,A))) by A2, Lm10;
hence |.(C - A).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A))) by Thm27; :: thesis: verum