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

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;

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

end;

then A11:
( B,D,C is_a_triangle & B,A,C is_a_triangle )
by A1, MENELAUS:15;A6: now :: thesis: ( D <> B & B <> C & D <> C )

then A7:
D,B,C are_mutually_distinct
;
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;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

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

hence
D,B,C is_a_triangle
by A7, EUCLID_6:20; :: thesis: verumhereby :: 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 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;( B in LSeg (D,B) & B <> C ) by A6, RLTOPSP1:68;

hence contradiction by A6, A1, A2, A8, EUCLID_6:30; :: thesis: verum

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;( C in LSeg (D,C) & C <> D ) by A3, RLTOPSP1:68;

hence contradiction by A6, A1, A2, A9, EUCLID_6:30; :: thesis: verum

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;( D in LSeg (B,D) & B <> D ) by A6, RLTOPSP1:68;

hence contradiction by A6, A1, A2, A10, EUCLID_6:30; :: thesis: verum

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 )

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;
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;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

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;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

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) )

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: verumassume 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;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