let p1, p2, p3, p4, p be Point of (TOP-REAL 2); for a, b, r being Real st p1 in circle (a,b,r) & p2 in circle (a,b,r) & p3 in circle (a,b,r) & p4 in circle (a,b,r) & p in LSeg (p1,p3) & p in LSeg (p2,p4) & p1,p2,p3,p4 are_mutually_distinct holds
angle (p1,p4,p2) = angle (p1,p3,p2)
let a, b, r be Real; ( p1 in circle (a,b,r) & p2 in circle (a,b,r) & p3 in circle (a,b,r) & p4 in circle (a,b,r) & p in LSeg (p1,p3) & p in LSeg (p2,p4) & p1,p2,p3,p4 are_mutually_distinct implies angle (p1,p4,p2) = angle (p1,p3,p2) )
assume that
A1:
p1 in circle (a,b,r)
and
A2:
p2 in circle (a,b,r)
and
A3:
p3 in circle (a,b,r)
and
A4:
p4 in circle (a,b,r)
; ( not p in LSeg (p1,p3) or not p in LSeg (p2,p4) or not p1,p2,p3,p4 are_mutually_distinct or angle (p1,p4,p2) = angle (p1,p3,p2) )
A5:
(LSeg (p1,p3)) \ {p1,p3} c= inside_of_circle (a,b,r)
by A1, A3, TOPREAL9:60;
assume that
A6:
p in LSeg (p1,p3)
and
A7:
p in LSeg (p2,p4)
; ( not p1,p2,p3,p4 are_mutually_distinct or angle (p1,p4,p2) = angle (p1,p3,p2) )
assume A8:
p1,p2,p3,p4 are_mutually_distinct
; angle (p1,p4,p2) = angle (p1,p3,p2)
then A9:
p1 <> p2
by ZFMISC_1:def 6;
A10:
p3 <> p4
by A8, ZFMISC_1:def 6;
A11:
p1 <> p4
by A8, ZFMISC_1:def 6;
A12:
p2 <> p4
by A8, ZFMISC_1:def 6;
A13:
p1 <> p3
by A8, ZFMISC_1:def 6;
A14:
inside_of_circle (a,b,r) misses circle (a,b,r)
by TOPREAL9:54;
A15:
(LSeg (p2,p4)) \ {p2,p4} c= inside_of_circle (a,b,r)
by A2, A4, TOPREAL9:60;
A16:
( p <> p1 & p <> p4 )
proof
assume A17:
(
p = p1 or
p = p4 )
;
contradiction
per cases
( p = p1 or p = p4 )
by A17;
suppose A18:
p = p1
;
contradiction
not
p1 in {p2,p4}
by A9, A11, TARSKI:def 2;
then
p1 in (LSeg (p2,p4)) \ {p2,p4}
by A7, A18, XBOOLE_0:def 5;
then
p1 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r))
by A1, A15, XBOOLE_0:def 4;
hence
contradiction
by A14, XBOOLE_0:def 7;
verum end; suppose A19:
p = p4
;
contradiction
not
p4 in {p1,p3}
by A11, A10, TARSKI:def 2;
then
p4 in (LSeg (p1,p3)) \ {p1,p3}
by A6, A19, XBOOLE_0:def 5;
then
p4 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r))
by A4, A5, XBOOLE_0:def 4;
hence
contradiction
by A14, XBOOLE_0:def 7;
verum end; end;
end;
then A20:
p1,p4,p are_mutually_distinct
by A11, ZFMISC_1:def 5;
A21:
p4,p,p1 are_mutually_distinct
by A11, A16, ZFMISC_1:def 5;
A22:
angle (p1,p4,p) = angle (p1,p4,p2)
by A7, A16, Th10;
A23:
p2 <> p3
by A8, ZFMISC_1:def 6;
A24:
( p <> p2 & p <> p3 )
proof
assume A25:
(
p = p2 or
p = p3 )
;
contradiction
per cases
( p = p3 or p = p2 )
by A25;
suppose A26:
p = p3
;
contradiction
not
p3 in {p2,p4}
by A23, A10, TARSKI:def 2;
then
p3 in (LSeg (p2,p4)) \ {p2,p4}
by A7, A26, XBOOLE_0:def 5;
then
p3 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r))
by A3, A15, XBOOLE_0:def 4;
hence
contradiction
by A14, XBOOLE_0:def 7;
verum end; suppose A27:
p = p2
;
contradiction
not
p2 in {p1,p3}
by A9, A23, TARSKI:def 2;
then
p2 in (LSeg (p1,p3)) \ {p1,p3}
by A6, A27, XBOOLE_0:def 5;
then
p2 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r))
by A2, A5, XBOOLE_0:def 4;
hence
contradiction
by A14, XBOOLE_0:def 7;
verum end; end;
end;
then A28:
angle (p4,p,p1) = angle (p2,p,p3)
by A6, A7, A16, Th15;
A29:
p,p3,p2 are_mutually_distinct
by A23, A24, ZFMISC_1:def 5;
A30:
p2,p,p3 are_mutually_distinct
by A23, A24, ZFMISC_1:def 5;
A31:
angle (p,p3,p2) = angle (p1,p3,p2)
by A6, A24, Th9;
per cases
( angle (p1,p4,p2) = angle (p1,p3,p2) or angle (p1,p4,p2) = (angle (p1,p3,p2)) - PI or angle (p1,p4,p2) = (angle (p1,p3,p2)) + PI )
by A1, A2, A3, A4, A13, A11, A23, A12, Th34;
suppose A32:
angle (
p1,
p4,
p2)
= (angle (p1,p3,p2)) - PI
;
angle (p1,p4,p2) = angle (p1,p3,p2)
angle (
p1,
p3,
p2)
< 2
* PI
by COMPLEX2:70;
then
(angle (p1,p3,p2)) - PI < (2 * PI) - PI
by XREAL_1:9;
then
angle (
p2,
p,
p3)
<= PI
by A22, A28, A20, A32, Th23;
then A33:
angle (
p1,
p3,
p2)
<= PI
by A31, A30, Th23;
A34:
not
p3 in {p1,p2}
by A13, A23, TARSKI:def 2;
angle (
p1,
p4,
p2)
>= 0
by COMPLEX2:70;
then
((angle (p1,p3,p2)) - PI) + PI >= 0 + PI
by A32, XREAL_1:6;
then
p3 in LSeg (
p1,
p2)
by A33, Th11, XXREAL_0:1;
then A35:
p3 in (LSeg (p1,p2)) \ {p1,p2}
by A34, XBOOLE_0:def 5;
(LSeg (p1,p2)) \ {p1,p2} c= inside_of_circle (
a,
b,
r)
by A1, A2, TOPREAL9:60;
then
(
inside_of_circle (
a,
b,
r)
misses circle (
a,
b,
r) &
p3 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r)) )
by A3, A35, TOPREAL9:54, XBOOLE_0:def 4;
hence
angle (
p1,
p4,
p2)
= angle (
p1,
p3,
p2)
by XBOOLE_0:def 7;
verum end; suppose A36:
angle (
p1,
p4,
p2)
= (angle (p1,p3,p2)) + PI
;
angle (p1,p4,p2) = angle (p1,p3,p2)
angle (
p1,
p4,
p2)
< 2
* PI
by COMPLEX2:70;
then
(angle (p1,p4,p2)) - PI < (2 * PI) - PI
by XREAL_1:9;
then
angle (
p4,
p,
p1)
<= PI
by A31, A28, A29, A36, Th23;
then A37:
angle (
p1,
p4,
p2)
<= PI
by A22, A21, Th23;
A38:
not
p4 in {p1,p2}
by A11, A12, TARSKI:def 2;
angle (
p1,
p3,
p2)
>= 0
by COMPLEX2:70;
then
((angle (p1,p4,p2)) - PI) + PI >= 0 + PI
by A36, XREAL_1:6;
then
p4 in LSeg (
p1,
p2)
by A37, Th11, XXREAL_0:1;
then A39:
p4 in (LSeg (p1,p2)) \ {p1,p2}
by A38, XBOOLE_0:def 5;
(LSeg (p1,p2)) \ {p1,p2} c= inside_of_circle (
a,
b,
r)
by A1, A2, TOPREAL9:60;
then
(
inside_of_circle (
a,
b,
r)
misses circle (
a,
b,
r) &
p4 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r)) )
by A4, A39, TOPREAL9:54, XBOOLE_0:def 4;
hence
angle (
p1,
p4,
p2)
= angle (
p1,
p3,
p2)
by XBOOLE_0:def 7;
verum end; end;