let C be Simple_closed_curve; North_Arc C c= C
A1:
North_Arc C = Lim_inf (Upper_Appr C)
by JORDAN19:def 3;
reconsider OO = BDD C as Subset of (TopSpaceMetr (Euclid 2)) by Lm4;
let x be object ; TARSKI:def 3 ( not x in North_Arc C or x in C )
assume A2:
x in North_Arc C
; x in C
assume A3:
not x in C
; contradiction
reconsider x = x as Point of (TOP-REAL 2) by A2;
A4:
x in C `
by A3, SUBSET_1:29;
A5:
(BDD C) \/ (UBD C) = C `
by JORDAN2C:27;
reconsider e = x as Point of (Euclid 2) by EUCLID:67;
per cases
( x in BDD C or x in UBD C )
by A4, A5, XBOOLE_0:def 3;
suppose A6:
x in BDD C
;
contradiction
OO is
open
by Lm4, PRE_TOPC:30;
then consider r being
Real such that A7:
r > 0
and A8:
Ball (
e,
r)
c= BDD C
by A6, TOPMETR:15;
consider k being
Nat such that A9:
for
m being
Nat st
m > k holds
(Upper_Appr C) . m meets Ball (
e,
r)
by A2, A1, A7, KURATO_2:14;
A10:
Upper_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1)))
by JORDAN6:61;
A11:
(Upper_Appr C) . (k + 1) = Upper_Arc (L~ (Cage (C,(k + 1))))
by JORDAN19:def 1;
A12:
k + 0 < k + 1
by XREAL_1:8;
Ball (
e,
r)
misses L~ (Cage (C,(k + 1)))
by A8, JORDAN10:19, XBOOLE_1:63;
hence
contradiction
by A9, A12, A11, A10, XBOOLE_1:63;
verum end; suppose A13:
x in UBD C
;
contradiction
union (UBD-Family C) = UBD C
by JORDAN10:14;
then consider A being
set such that A14:
x in A
and A15:
A in UBD-Family C
by A13, TARSKI:def 4;
UBD-Family C = { (UBD (L~ (Cage (C,m)))) where m is Nat : verum }
by JORDAN10:def 1;
then consider m being
Nat such that A16:
A = UBD (L~ (Cage (C,m)))
by A15;
reconsider OO =
LeftComp (Cage (C,m)) as
Subset of
(TopSpaceMetr (Euclid 2)) by Lm4;
A17:
OO is
open
by Lm4, PRE_TOPC:30;
x in LeftComp (Cage (C,m))
by A14, A16, GOBRD14:36;
then consider r being
Real such that A18:
r > 0
and A19:
Ball (
e,
r)
c= LeftComp (Cage (C,m))
by A17, TOPMETR:15;
consider k being
Nat such that A20:
for
m being
Nat st
m > k holds
(Upper_Appr C) . m meets Ball (
e,
r)
by A2, A1, A18, KURATO_2:14;
thus
contradiction
verumproof
per cases
( m > k or m <= k )
;
suppose A21:
m > k
;
contradictionA22:
(Upper_Appr C) . m = Upper_Arc (L~ (Cage (C,m)))
by JORDAN19:def 1;
A23:
Upper_Arc (L~ (Cage (C,m))) c= L~ (Cage (C,m))
by JORDAN6:61;
Ball (
e,
r)
misses L~ (Cage (C,m))
by A19, SPRECT_3:26, XBOOLE_1:63;
hence
contradiction
by A20, A21, A22, A23, XBOOLE_1:63;
verum end; suppose
m <= k
;
contradictionthen
LeftComp (Cage (C,m)) c= LeftComp (Cage (C,k))
by JORDAN1H:47;
then A24:
Ball (
e,
r)
c= LeftComp (Cage (C,k))
by A19;
A25:
k + 0 < k + 1
by XREAL_1:8;
then
LeftComp (Cage (C,k)) c= LeftComp (Cage (C,(k + 1)))
by JORDAN1H:47;
then
Ball (
e,
r)
c= LeftComp (Cage (C,(k + 1)))
by A24;
then A26:
Ball (
e,
r)
misses L~ (Cage (C,(k + 1)))
by SPRECT_3:26, XBOOLE_1:63;
A27:
Upper_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1)))
by JORDAN6:61;
(Upper_Appr C) . (k + 1) = Upper_Arc (L~ (Cage (C,(k + 1))))
by JORDAN19:def 1;
hence
contradiction
by A20, A25, A26, A27, XBOOLE_1:63;
verum end;
end; end;