let a be Real; :: thesis: for A, B, C, D being Point of (TOP-REAL 2)
for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) & C <> D & not the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) holds
the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C))
let A, B, C, D be Point of (TOP-REAL 2); :: thesis: for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) & C <> D & not the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) holds
the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C))
let b, r be Real; :: thesis: ( A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) & C <> D & not the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) implies the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C)) )
assume that
A1: ( A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) ) and
A2: ( A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) ) and
A3: C <> D ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) or the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C)) )
A4: B,A,C is_a_triangle by A1, MENELAUS:15;
A5: D,B,C is_a_triangle

proof

A6: now :: thesis: ( D <> B & B <> C & D <> C )

A,B,D are_mutually_distinct by A2, EUCLID_6:20;
hence D <> B ; :: thesis: ( B <> C & D <> C )
A,B,C are_mutually_distinct by A1, EUCLID_6:20;
hence B <> C ; :: thesis: D <> C
thus D <> C by A3; :: thesis: verum

end;

then A7: D,B,C are_mutually_distinct ;

now :: thesis: ( not angle (D,B,C) = PI & not angle (B,C,D) = PI & not angle (C,D,B) = PI )

hereby :: thesis: verum

assume ( angle (D,B,C) = PI or angle (B,C,D) = PI or angle (C,D,B) = PI ) ; :: thesis: contradiction

per cases then ( angle (D,B,C) = PI or angle (B,C,D) = PI or angle (C,D,B) = PI ) ;

suppose angle (D,B,C) = PI ; :: thesis: contradiction

then A8: B in LSeg (D,C) by EUCLID_6:11;
( B in LSeg (D,B) & B <> C ) by A6, RLTOPSP1:68;
hence contradiction by A6, A1, A2, A8, EUCLID_6:30; :: thesis: verum

end;

suppose angle (B,C,D) = PI ; :: thesis: contradiction

then A9: C in LSeg (B,D) by EUCLID_6:11;
( C in LSeg (D,C) & C <> D ) by A3, RLTOPSP1:68;
hence contradiction by A6, A1, A2, A9, EUCLID_6:30; :: thesis: verum

end;

suppose angle (C,D,B) = PI ; :: thesis: contradiction

then A10: D in LSeg (C,B) by EUCLID_6:11;
( D in LSeg (B,D) & B <> D ) by A6, RLTOPSP1:68;
hence contradiction by A6, A1, A2, A10, EUCLID_6:30; :: thesis: verum

end;

end;

end;

end;

hence D,B,C is_a_triangle by A7, EUCLID_6:20; :: thesis: verum

end;

then A11: ( B,D,C is_a_triangle & B,A,C is_a_triangle ) by A1, MENELAUS:15;
A12: ( the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C)) & the_diameter_of_the_circumcircle (D,B,C) = - (the_diameter_of_the_circumcircle (B,D,C)) ) by A1, A5, EUCLID10:47;

now :: thesis: ( A <> B & B <> C & A <> C & B <> D & C <> D )

A,B,C are_mutually_distinct by A1, EUCLID_6:20;
hence ( A <> B & B <> C & A <> C ) ; :: thesis: ( B <> D & C <> D )
D,B,C are_mutually_distinct by A5, EUCLID_6:20;
hence ( B <> D & C <> D ) ; :: thesis: verum

end;

then A13: ( angle (B,A,C) = angle (B,D,C) or angle (B,A,C) = (angle (B,D,C)) - PI or angle (B,A,C) = (angle (B,D,C)) + PI ) by A1, A2, EUCLID_6:34;

A14: now :: thesis: ( sin (angle (B,A,C)) = sin (angle (B,D,C)) implies the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) )

assume A15: sin (angle (B,A,C)) = sin (angle (B,D,C)) ; :: thesis: the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C)
thus the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C)) by A1, EUCLID10:47
.= - (- (|.(C - B).| / (sin (angle (B,A,C))))) by A4, EUCLID10:45
.= - (the_diameter_of_the_circumcircle (B,D,C)) by A11, EUCLID10:45, A15
.= the_diameter_of_the_circumcircle (D,B,C) by A5, EUCLID10:47 ; :: thesis: verum

end;

now :: thesis: ( sin (angle (B,A,C)) = - (sin (angle (B,D,C))) implies the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (B,D,C) )

assume A16: sin (angle (B,A,C)) = - (sin (angle (B,D,C))) ; :: thesis: the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (B,D,C)
thus the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C)) by A1, EUCLID10:47
.= - (- (|.(C - B).| / (sin (angle (B,A,C))))) by A11, EUCLID10:45
.= (- |.(C - B).|) / (sin (angle (B,D,C))) by A16, XCMPLX_1:192
.= - (|.(C - B).| / (sin (angle (B,D,C))))
.= the_diameter_of_the_circumcircle (B,D,C) by A11, EUCLID10:45 ; :: thesis: verum

end;

hence ( the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) or the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C)) ) by A13, Lm2, SIN_COS:79, A14, A12; :: thesis: verum