let a be Real; :: thesis: for A, B, C 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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r holds

the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)

let A, B, C 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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r holds

the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)

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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r implies the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

assume that

A1: A,B,C is_a_triangle and

A2: ( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) ) ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

A3: r is positive by A1, A2, EUCLID10:37;

then consider D being Point of (TOP-REAL 2) such that

A4: C <> D and

A5: D in circle (a,b,r) and

A6: |[a,b]| in LSeg (C,D) by A2, EUCLID_6:32;

A7: A,B,C are_mutually_distinct by A1, EUCLID_6:20;

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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r holds

the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)

let A, B, C 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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r holds

the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)

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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r implies the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

assume that

A1: A,B,C is_a_triangle and

A2: ( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) ) ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

A3: r is positive by A1, A2, EUCLID10:37;

then consider D being Point of (TOP-REAL 2) such that

A4: C <> D and

A5: D in circle (a,b,r) and

A6: |[a,b]| in LSeg (C,D) by A2, EUCLID_6:32;

A7: A,B,C are_mutually_distinct by A1, EUCLID_6:20;

per cases
( D = B or D <> B )
;

end;

suppose A8:
D = B
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then A9:
( B,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg (B,C) )
by A6, A7, A2, A3, EUCLID10:38;

A10: B,A,C is_a_triangle by A1, MENELAUS:15;

A11: the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C)) by A1, EUCLID10:47

.= - (|.(C - B).| / (sin (angle (C,A,B)))) by A10, EUCLID10:44 ;

( angle (B,A,C) in ].0,PI.[ or angle (B,A,C) in ].PI,(2 * PI).[ )

end;A10: B,A,C is_a_triangle by A1, MENELAUS:15;

A11: the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C)) by A1, EUCLID10:47

.= - (|.(C - B).| / (sin (angle (C,A,B)))) by A10, EUCLID10:44 ;

( angle (B,A,C) in ].0,PI.[ or angle (B,A,C) in ].PI,(2 * PI).[ )

proof

A12:
( ( 0 <= angle (B,A,C) & angle (B,A,C) < PI ) or angle (B,A,C) = PI or ( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI ) )
by EUCLID11:3;

( ( 0 < angle (B,A,C) & angle (B,A,C) < PI ) or ( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI ) ) by A12, A1, EUCLID10:30, A2, A7, EUCLID_6:35;

hence ( angle (B,A,C) in ].0,PI.[ or angle (B,A,C) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum

end;( ( 0 < angle (B,A,C) & angle (B,A,C) < PI ) or ( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI ) ) by A12, A1, EUCLID10:30, A2, A7, EUCLID_6:35;

hence ( angle (B,A,C) in ].0,PI.[ or angle (B,A,C) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum

per cases then
( angle (B,A,C) in ].0,PI.[ or angle (B,A,C) in ].PI,(2 * PI).[ )
;

end;

suppose A13:
angle (B,A,C) in ].0,PI.[
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then
( 0 < angle (B,A,C) & angle (B,A,C) < PI & B,A,C are_mutually_distinct )
by A7, XXREAL_1:4;

then ( 0 < angle (A,C,B) & angle (A,C,B) < PI ) by EUCLID11:5;

then A14: ( C,A,B is_a_triangle & angle (B,A,C) in ].0,PI.[ & angle (A,C,B) in ].0,PI.[ & |[a,b]| in LSeg (C,B) ) by A13, A1, MENELAUS:15, A6, A8, XXREAL_1:4;

angle (C,A,B) = (2 * PI) - (angle (B,A,C)) by A1, EUCLID10:31

.= (2 * PI) - (PI / 2) by A14, A2, EUCLID10:39

.= (3 * PI) / 2 ;

then the_diameter_of_the_circumcircle (A,B,C) = |.(B - C).| by EUCLID_6:43, A11, SIN_COS:77

.= 2 * r by A9, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum

end;then ( 0 < angle (A,C,B) & angle (A,C,B) < PI ) by EUCLID11:5;

then A14: ( C,A,B is_a_triangle & angle (B,A,C) in ].0,PI.[ & angle (A,C,B) in ].0,PI.[ & |[a,b]| in LSeg (C,B) ) by A13, A1, MENELAUS:15, A6, A8, XXREAL_1:4;

angle (C,A,B) = (2 * PI) - (angle (B,A,C)) by A1, EUCLID10:31

.= (2 * PI) - (PI / 2) by A14, A2, EUCLID10:39

.= (3 * PI) / 2 ;

then the_diameter_of_the_circumcircle (A,B,C) = |.(B - C).| by EUCLID_6:43, A11, SIN_COS:77

.= 2 * r by A9, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum

suppose
angle (B,A,C) in ].PI,(2 * PI).[
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then
( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI & B,A,C are_mutually_distinct )
by A7, XXREAL_1:4;

then ( PI < angle (A,C,B) & angle (A,C,B) < 2 * PI ) by EUCLID11:2, EUCLID11:8;

then ( (2 * PI) - (angle (A,C,B)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (A,C,B)) & angle (B,C,A) = (2 * PI) - (angle (A,C,B)) ) by A1, EUCLID10:31, XREAL_1:15, XREAL_1:50;

then ( 0 < angle (B,C,A) & angle (B,C,A) < PI & B,C,A are_mutually_distinct ) by A7;

then ( 0 < angle (A,B,C) & angle (A,B,C) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI ) by EUCLID11:5;

then ( B,A,C is_a_triangle & angle (C,A,B) in ].0,PI.[ & angle (A,B,C) in ].0,PI.[ & |[a,b]| in LSeg (B,C) ) by A1, MENELAUS:15, A6, A8, XXREAL_1:4;

then sin (angle (C,A,B)) = 1 by SIN_COS:77, A2, EUCLID10:39;

then the_diameter_of_the_circumcircle (A,B,C) = - |.(B - C).| by A11, EUCLID_6:43

.= - (2 * r) by A9, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum

end;then ( PI < angle (A,C,B) & angle (A,C,B) < 2 * PI ) by EUCLID11:2, EUCLID11:8;

then ( (2 * PI) - (angle (A,C,B)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (A,C,B)) & angle (B,C,A) = (2 * PI) - (angle (A,C,B)) ) by A1, EUCLID10:31, XREAL_1:15, XREAL_1:50;

then ( 0 < angle (B,C,A) & angle (B,C,A) < PI & B,C,A are_mutually_distinct ) by A7;

then ( 0 < angle (A,B,C) & angle (A,B,C) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI ) by EUCLID11:5;

then ( B,A,C is_a_triangle & angle (C,A,B) in ].0,PI.[ & angle (A,B,C) in ].0,PI.[ & |[a,b]| in LSeg (B,C) ) by A1, MENELAUS:15, A6, A8, XXREAL_1:4;

then sin (angle (C,A,B)) = 1 by SIN_COS:77, A2, EUCLID10:39;

then the_diameter_of_the_circumcircle (A,B,C) = - |.(B - C).| by A11, EUCLID_6:43

.= - (2 * r) by A9, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum

suppose A15:
D <> B
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then A16:
D,B,C are_mutually_distinct
by A4, A7;

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

then A21:
D,B,C is_a_triangle
by A16, EUCLID_6:20;hereby :: thesis: verum

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

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

end;

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

then A18:
B in LSeg (D,C)
by EUCLID_6:11;

( B in LSeg (D,B) & B <> C & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A7, RLTOPSP1:68;

hence contradiction by A15, A18, EUCLID_6:30; :: thesis: verum

end;( B in LSeg (D,B) & B <> C & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A7, RLTOPSP1:68;

hence contradiction by A15, A18, EUCLID_6:30; :: thesis: verum

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

then A19:
C in LSeg (B,D)
by EUCLID_6:11;

( C in LSeg (B,C) & C <> D & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A4, RLTOPSP1:68;

hence contradiction by A7, A19, EUCLID_6:30; :: thesis: verum

end;( C in LSeg (B,C) & C <> D & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A4, RLTOPSP1:68;

hence contradiction by A7, A19, EUCLID_6:30; :: thesis: verum

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

then A20:
D in LSeg (C,B)
by EUCLID_6:11;

( D in LSeg (C,D) & D <> B & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A15, A2, A5, RLTOPSP1:68;

hence contradiction by A4, A20, EUCLID_6:30; :: thesis: verum

end;( D in LSeg (C,D) & D <> B & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A15, A2, A5, RLTOPSP1:68;

hence contradiction by A4, A20, EUCLID_6:30; :: thesis: verum

per cases
( A = D or A <> D )
;

end;

suppose A22:
A = D
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

A23:
( A,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg (A,C) )
by A22, A6, A7, A2, A3, EUCLID10:38;

A24: the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A))) by A1, EUCLID10:44;

( angle (C,B,A) in ].0,PI.[ or angle (C,B,A) in ].PI,(2 * PI).[ )

end;A24: the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A))) by A1, EUCLID10:44;

( angle (C,B,A) in ].0,PI.[ or angle (C,B,A) in ].PI,(2 * PI).[ )

proof

( ( 0 <= angle (C,B,A) & angle (C,B,A) < PI ) or angle (C,B,A) = PI or ( PI < angle (C,B,A) & angle (C,B,A) < 2 * PI ) )
by EUCLID11:3;

then ( ( 0 < angle (C,B,A) & angle (C,B,A) < PI ) or ( PI < angle (C,B,A) & angle (C,B,A) < 2 * PI ) ) by A2, A7, EUCLID_6:35, A1, EUCLID10:30;

hence ( angle (C,B,A) in ].0,PI.[ or angle (C,B,A) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum

end;then ( ( 0 < angle (C,B,A) & angle (C,B,A) < PI ) or ( PI < angle (C,B,A) & angle (C,B,A) < 2 * PI ) ) by A2, A7, EUCLID_6:35, A1, EUCLID10:30;

hence ( angle (C,B,A) in ].0,PI.[ or angle (C,B,A) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum

per cases then
( angle (C,B,A) in ].0,PI.[ or angle (C,B,A) in ].PI,(2 * PI).[ )
;

end;

suppose A25:
angle (C,B,A) in ].0,PI.[
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then
( 0 < angle (C,B,A) & angle (C,B,A) < PI & C,B,A are_mutually_distinct )
by A7, XXREAL_1:4;

then ( 0 < angle (B,A,C) & angle (B,A,C) < PI ) by EUCLID11:5;

then ( C,B,A is_a_triangle & angle (C,B,A) in ].0,PI.[ & angle (B,A,C) in ].0,PI.[ & |[a,b]| in LSeg (A,C) ) by A25, A1, MENELAUS:15, A6, A22, XXREAL_1:4;

then the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / 1 by A24, A1, A2, EUCLID10:39, SIN_COS:77

.= |.(A - C).| by EUCLID_6:43

.= 2 * r by A23, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum

end;then ( 0 < angle (B,A,C) & angle (B,A,C) < PI ) by EUCLID11:5;

then ( C,B,A is_a_triangle & angle (C,B,A) in ].0,PI.[ & angle (B,A,C) in ].0,PI.[ & |[a,b]| in LSeg (A,C) ) by A25, A1, MENELAUS:15, A6, A22, XXREAL_1:4;

then the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / 1 by A24, A1, A2, EUCLID10:39, SIN_COS:77

.= |.(A - C).| by EUCLID_6:43

.= 2 * r by A23, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum

suppose
angle (C,B,A) in ].PI,(2 * PI).[
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then
( PI < angle (C,B,A) & 2 * PI <= 2 * PI & angle (C,B,A) < 2 * PI )
by XXREAL_1:4;

then A26: ( (2 * PI) - (angle (C,B,A)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,A)) & angle (A,B,C) = (2 * PI) - (angle (C,B,A)) ) by A1, EUCLID10:31, XREAL_1:15, XREAL_1:50;

then ( 0 < angle (B,C,A) & angle (B,C,A) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI ) by A7, EUCLID11:5;

then A27: ( C,B,A is_a_triangle & angle (A,B,C) in ].0,PI.[ & angle (B,C,A) in ].0,PI.[ & |[a,b]| in LSeg (C,A) ) by A26, XXREAL_1:4, A1, MENELAUS:15, A6, A22;

angle (C,B,A) = (2 * PI) - (angle (A,B,C)) by A1, EUCLID10:31

.= (2 * PI) - (PI / 2) by A27, A2, EUCLID10:39

.= (3 * PI) / 2 ;

then the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (- 1) by A1, EUCLID10:44, SIN_COS:77

.= - |.(C - A).|

.= - |.(A - C).| by EUCLID_6:43

.= - (2 * r) by A23, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum

end;then A26: ( (2 * PI) - (angle (C,B,A)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,A)) & angle (A,B,C) = (2 * PI) - (angle (C,B,A)) ) by A1, EUCLID10:31, XREAL_1:15, XREAL_1:50;

then ( 0 < angle (B,C,A) & angle (B,C,A) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI ) by A7, EUCLID11:5;

then A27: ( C,B,A is_a_triangle & angle (A,B,C) in ].0,PI.[ & angle (B,C,A) in ].0,PI.[ & |[a,b]| in LSeg (C,A) ) by A26, XXREAL_1:4, A1, MENELAUS:15, A6, A22;

angle (C,B,A) = (2 * PI) - (angle (A,B,C)) by A1, EUCLID10:31

.= (2 * PI) - (PI / 2) by A27, A2, EUCLID10:39

.= (3 * PI) / 2 ;

then the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (- 1) by A1, EUCLID10:44, SIN_COS:77

.= - |.(C - A).|

.= - |.(A - C).| by EUCLID_6:43

.= - (2 * r) by A23, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum

suppose A28:
A <> D
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then A29:
A,B,D are_mutually_distinct
by A15, A7;

A30: D,B,C are_mutually_distinct by A15, A4, A7;

A31: ( D,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg (D,C) ) by A6, A5, A4, A2, A3, EUCLID10:38;

A32: ( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ )

end;A30: D,B,C are_mutually_distinct by A15, A4, A7;

A31: ( D,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg (D,C) ) by A6, A5, A4, A2, A3, EUCLID10:38;

A32: ( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ )

proof

( ( 0 <= angle (C,B,D) & angle (C,B,D) < PI ) or angle (C,B,D) = PI or ( PI < angle (C,B,D) & angle (C,B,D) < 2 * PI ) )
by EUCLID11:3;

then ( ( 0 < angle (C,B,D) & angle (C,B,D) < PI ) or ( PI < angle (C,B,D) & angle (C,B,D) < 2 * PI ) ) by A21, EUCLID10:30, A5, A2, EUCLID_6:35, A15, A7;

hence ( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum

end;then ( ( 0 < angle (C,B,D) & angle (C,B,D) < PI ) or ( PI < angle (C,B,D) & angle (C,B,D) < 2 * PI ) ) by A21, EUCLID10:30, A5, A2, EUCLID_6:35, A15, A7;

hence ( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum

now :: thesis: ( not angle (A,B,D) = PI & not angle (B,D,A) = PI & not angle (D,A,B) = PI )end;

then
( A,B,D is_a_triangle & A,B,C is_a_triangle )
by A29, A1, EUCLID_6:20;hereby :: thesis: verum

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

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

end;

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

then A33:
B in LSeg (A,D)
by EUCLID_6:11;

( B in LSeg (A,B) & B <> D & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A15, RLTOPSP1:68;

hence contradiction by A7, A33, EUCLID_6:30; :: thesis: verum

end;( B in LSeg (A,B) & B <> D & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A15, RLTOPSP1:68;

hence contradiction by A7, A33, EUCLID_6:30; :: thesis: verum

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

then A34:
D in LSeg (B,A)
by EUCLID_6:11;

( D in LSeg (B,D) & D <> A & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A28, RLTOPSP1:68;

hence contradiction by A15, A34, EUCLID_6:30; :: thesis: verum

end;( D in LSeg (B,D) & D <> A & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A28, RLTOPSP1:68;

hence contradiction by A15, A34, EUCLID_6:30; :: thesis: verum

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

then A35:
A in LSeg (D,B)
by EUCLID_6:11;

( A in LSeg (D,A) & A <> B & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A7, RLTOPSP1:68;

hence contradiction by A28, A35, EUCLID_6:30; :: thesis: verum

end;( A in LSeg (D,A) & A <> B & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A7, RLTOPSP1:68;

hence contradiction by A28, A35, EUCLID_6:30; :: thesis: verum

per cases then
( 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 A4, A5, A2, Th51;

end;

suppose A36:
the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C)
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

end;

per cases
( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ )
by A32;

end;

suppose A37:
angle (C,B,D) in ].0,PI.[
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / 1 by A17, A16, EUCLID_6:20, EUCLID10:44

.= |.(D - C).| by EUCLID_6:43

.= 2 * r by A31, A5, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A36; :: thesis: verum

end;

now :: thesis: ( angle (C,B,D) in ].0,PI.[ & angle (B,D,C) in ].0,PI.[ & |[a,b]| in LSeg (D,C) )

then
sin (angle (C,B,D)) = 1
by SIN_COS:77, A17, A16, EUCLID_6:20, A5, A2, EUCLID10:39;thus
angle (C,B,D) in ].0,PI.[
by A37; :: thesis: ( angle (B,D,C) in ].0,PI.[ & |[a,b]| in LSeg (D,C) )

( 0 < angle (C,B,D) & angle (C,B,D) < PI & C,B,D are_mutually_distinct ) by A37, A15, A4, A7, XXREAL_1:4;

then ( 0 < angle (B,D,C) & angle (B,D,C) < PI ) by EUCLID11:5;

hence angle (B,D,C) in ].0,PI.[ by XXREAL_1:4; :: thesis: |[a,b]| in LSeg (D,C)

thus |[a,b]| in LSeg (D,C) by A6; :: thesis: verum

end;( 0 < angle (C,B,D) & angle (C,B,D) < PI & C,B,D are_mutually_distinct ) by A37, A15, A4, A7, XXREAL_1:4;

then ( 0 < angle (B,D,C) & angle (B,D,C) < PI ) by EUCLID11:5;

hence angle (B,D,C) in ].0,PI.[ by XXREAL_1:4; :: thesis: |[a,b]| in LSeg (D,C)

thus |[a,b]| in LSeg (D,C) by A6; :: thesis: verum

then the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / 1 by A17, A16, EUCLID_6:20, EUCLID10:44

.= |.(D - C).| by EUCLID_6:43

.= 2 * r by A31, A5, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A36; :: thesis: verum

suppose
angle (C,B,D) in ].PI,(2 * PI).[
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then
( PI < angle (C,B,D) & 2 * PI <= 2 * PI & angle (C,B,D) < 2 * PI )
by XXREAL_1:4;

then A38: ( (2 * PI) - (angle (C,B,D)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,D)) & angle (D,B,C) = (2 * PI) - (angle (C,B,D)) ) by A21, EUCLID10:31, XREAL_1:15, XREAL_1:50;

( 0 < angle (B,C,D) & angle (B,C,D) < PI & 0 < angle (C,D,B) & angle (C,D,B) < PI ) by A38, A30, EUCLID11:5;

then A39: ( C,B,D is_a_triangle & angle (D,B,C) in ].0,PI.[ & angle (B,C,D) in ].0,PI.[ & |[a,b]| in LSeg (C,D) ) by A38, XXREAL_1:4, A21, MENELAUS:15, A6;

A40: angle (C,B,D) = (2 * PI) - (angle (D,B,C)) by A21, EUCLID10:31

.= (2 * PI) - (PI / 2) by A39, A5, A2, EUCLID10:39

.= (3 * PI) / 2 ;

the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / (sin (angle (C,B,D))) by A17, A16, EUCLID_6:20, EUCLID10:44

.= - (|.(C - D).| / 1) by A40, SIN_COS:77

.= - |.(D - C).| by EUCLID_6:43

.= - (2 * r) by A31, A5, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A36; :: thesis: verum

end;then A38: ( (2 * PI) - (angle (C,B,D)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,D)) & angle (D,B,C) = (2 * PI) - (angle (C,B,D)) ) by A21, EUCLID10:31, XREAL_1:15, XREAL_1:50;

( 0 < angle (B,C,D) & angle (B,C,D) < PI & 0 < angle (C,D,B) & angle (C,D,B) < PI ) by A38, A30, EUCLID11:5;

then A39: ( C,B,D is_a_triangle & angle (D,B,C) in ].0,PI.[ & angle (B,C,D) in ].0,PI.[ & |[a,b]| in LSeg (C,D) ) by A38, XXREAL_1:4, A21, MENELAUS:15, A6;

A40: angle (C,B,D) = (2 * PI) - (angle (D,B,C)) by A21, EUCLID10:31

.= (2 * PI) - (PI / 2) by A39, A5, A2, EUCLID10:39

.= (3 * PI) / 2 ;

the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / (sin (angle (C,B,D))) by A17, A16, EUCLID_6:20, EUCLID10:44

.= - (|.(C - D).| / 1) by A40, SIN_COS:77

.= - |.(D - C).| by EUCLID_6:43

.= - (2 * r) by A31, A5, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A36; :: thesis: verum

suppose A41:
the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C))
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

end;

per cases
( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ )
by A32;

end;

suppose A42:
angle (C,B,D) in ].0,PI.[
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

.= |.(C - D).| / 1 by A43, SIN_COS:77, A17, A16, EUCLID_6:20, A5, A2, EUCLID10:39

.= |.(D - C).| by EUCLID_6:43

.= 2 * r by A31, A2, A5, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A41; :: thesis: verum

end;

A43: now :: thesis: ( angle (C,B,D) in ].0,PI.[ & angle (B,D,C) in ].0,PI.[ & |[a,b]| in LSeg (D,C) )

the_diameter_of_the_circumcircle (D,B,C) =
|.(C - D).| / (sin (angle (C,B,D)))
by A17, A16, EUCLID_6:20, EUCLID10:44
thus
angle (C,B,D) in ].0,PI.[
by A42; :: thesis: ( angle (B,D,C) in ].0,PI.[ & |[a,b]| in LSeg (D,C) )

( 0 < angle (C,B,D) & angle (C,B,D) < PI & C,B,D are_mutually_distinct ) by A42, A15, A4, A7, XXREAL_1:4;

then ( 0 < angle (B,D,C) & angle (B,D,C) < PI ) by EUCLID11:5;

hence angle (B,D,C) in ].0,PI.[ by XXREAL_1:4; :: thesis: |[a,b]| in LSeg (D,C)

thus |[a,b]| in LSeg (D,C) by A6; :: thesis: verum

end;( 0 < angle (C,B,D) & angle (C,B,D) < PI & C,B,D are_mutually_distinct ) by A42, A15, A4, A7, XXREAL_1:4;

then ( 0 < angle (B,D,C) & angle (B,D,C) < PI ) by EUCLID11:5;

hence angle (B,D,C) in ].0,PI.[ by XXREAL_1:4; :: thesis: |[a,b]| in LSeg (D,C)

thus |[a,b]| in LSeg (D,C) by A6; :: thesis: verum

.= |.(C - D).| / 1 by A43, SIN_COS:77, A17, A16, EUCLID_6:20, A5, A2, EUCLID10:39

.= |.(D - C).| by EUCLID_6:43

.= 2 * r by A31, A2, A5, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A41; :: thesis: verum

suppose
angle (C,B,D) in ].PI,(2 * PI).[
; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )

then
( PI < angle (C,B,D) & 2 * PI <= 2 * PI & angle (C,B,D) < 2 * PI )
by XXREAL_1:4;

then A44: ( (2 * PI) - (angle (C,B,D)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,D)) & angle (D,B,C) = (2 * PI) - (angle (C,B,D)) ) by A21, EUCLID10:31, XREAL_1:15, XREAL_1:50;

then ( 0 < angle (B,C,D) & angle (B,C,D) < PI & 0 < angle (C,D,B) & angle (C,D,B) < PI ) by A30, EUCLID11:5;

then A45: ( C,B,D is_a_triangle & angle (D,B,C) in ].0,PI.[ & angle (B,C,D) in ].0,PI.[ & |[a,b]| in LSeg (C,D) ) by XXREAL_1:4, A44, A21, MENELAUS:15, A6;

A46: angle (C,B,D) = (2 * PI) - (angle (D,B,C)) by A21, EUCLID10:31

.= (2 * PI) - (PI / 2) by A45, A5, A2, EUCLID10:39

.= (3 * PI) / 2 ;

the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / (- 1) by A46, SIN_COS:77, A17, A16, EUCLID_6:20, EUCLID10:44

.= - |.(C - D).|

.= - |.(D - C).| by EUCLID_6:43

.= - (2 * r) by A31, A5, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A41; :: thesis: verum

end;then A44: ( (2 * PI) - (angle (C,B,D)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,D)) & angle (D,B,C) = (2 * PI) - (angle (C,B,D)) ) by A21, EUCLID10:31, XREAL_1:15, XREAL_1:50;

then ( 0 < angle (B,C,D) & angle (B,C,D) < PI & 0 < angle (C,D,B) & angle (C,D,B) < PI ) by A30, EUCLID11:5;

then A45: ( C,B,D is_a_triangle & angle (D,B,C) in ].0,PI.[ & angle (B,C,D) in ].0,PI.[ & |[a,b]| in LSeg (C,D) ) by XXREAL_1:4, A44, A21, MENELAUS:15, A6;

A46: angle (C,B,D) = (2 * PI) - (angle (D,B,C)) by A21, EUCLID10:31

.= (2 * PI) - (PI / 2) by A45, A5, A2, EUCLID10:39

.= (3 * PI) / 2 ;

the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / (- 1) by A46, SIN_COS:77, A17, A16, EUCLID_6:20, EUCLID10:44

.= - |.(C - D).|

.= - |.(D - C).| by EUCLID_6:43

.= - (2 * r) by A31, A5, A2, A3, EUCLID10:58 ;

hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A41; :: thesis: verum