let C be Simple_closed_curve; :: thesis: South_Arc C c= C
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in South_Arc C or x in C )
assume A1:
x in South_Arc C
; :: thesis: x in C
assume A2:
not x in C
; :: thesis: contradiction
reconsider x = x as Point of (TOP-REAL 2) by A1;
reconsider e = x as Point of (Euclid 2) by EUCLID:71;
A3:
South_Arc C = Lim_inf (Lower_Appr C)
by JORDAN19:def 4;
A4:
x in C `
by A2, SUBSET_1:50;
A5:
(BDD C) \/ (UBD C) = C `
by JORDAN2C:31;
per cases
( x in BDD C or x in UBD C )
by A4, A5, XBOOLE_0:def 3;
suppose S:
x in BDD C
;
:: thesis: contradictionreconsider OO =
BDD C as
Subset of
(TopSpaceMetr (Euclid 2)) by XX;
OO is
open
by XX, PRE_TOPC:60;
then consider r being
real number such that A6:
r > 0
and A7:
Ball e,
r c= BDD C
by S, TOPMETR:22;
consider k being
Element of
NAT such that A8:
for
m being
Element of
NAT st
m > k holds
(Lower_Appr C) . m meets Ball e,
r
by A1, A3, A6, KURATO_2:48;
A9:
k + 0 < k + 1
by XREAL_1:10;
A10:
Ball e,
r misses L~ (Cage C,(k + 1))
by A7, JORDAN10:19, XBOOLE_1:63;
A11:
(Lower_Appr C) . (k + 1) = Lower_Arc (L~ (Cage C,(k + 1)))
by JORDAN19:def 2;
Lower_Arc (L~ (Cage C,(k + 1))) c= L~ (Cage C,(k + 1))
by JORDAN6:76;
hence
contradiction
by A8, A9, A10, A11, XBOOLE_1:63;
:: thesis: verum end; suppose A12:
x in UBD C
;
:: thesis: contradiction
union (UBD-Family C) = UBD C
by JORDAN10:14;
then consider A being
set such that A13:
x in A
and A14:
A in UBD-Family C
by A12, TARSKI:def 4;
UBD-Family C = { (UBD (L~ (Cage C,m))) where m is Element of NAT : verum }
by JORDAN10:def 1;
then consider m being
Element of
NAT such that A15:
A = UBD (L~ (Cage C,m))
by A14;
reconsider OO =
LeftComp (Cage C,m) as
Subset of
(TopSpaceMetr (Euclid 2)) by XX;
UU:
OO is
open
by XX, PRE_TOPC:60;
x in LeftComp (Cage C,m)
by A13, A15, GOBRD14:46;
then consider r being
real number such that A16:
r > 0
and A17:
Ball e,
r c= LeftComp (Cage C,m)
by UU, XX, TOPMETR:22;
consider k being
Element of
NAT such that A18:
for
m being
Element of
NAT st
m > k holds
(Lower_Appr C) . m meets Ball e,
r
by A1, A3, A16, KURATO_2:48;
thus
contradiction
:: thesis: verumproof
per cases
( m > k or m <= k )
;
suppose A19:
m > k
;
:: thesis: contradictionA20:
Ball e,
r misses L~ (Cage C,m)
by A17, SPRECT_3:43, XBOOLE_1:63;
A21:
(Lower_Appr C) . m = Lower_Arc (L~ (Cage C,m))
by JORDAN19:def 2;
Lower_Arc (L~ (Cage C,m)) c= L~ (Cage C,m)
by JORDAN6:76;
hence
contradiction
by A18, A19, A20, A21, XBOOLE_1:63;
:: thesis: verum end; suppose
m <= k
;
:: thesis: contradictionthen A22:
LeftComp (Cage C,m) c= LeftComp (Cage C,k)
by JORDAN1H:55;
A23:
k + 0 < k + 1
by XREAL_1:10;
then A24:
LeftComp (Cage C,k) c= LeftComp (Cage C,(k + 1))
by JORDAN1H:55;
Ball e,
r c= LeftComp (Cage C,k)
by A17, A22, XBOOLE_1:1;
then
Ball e,
r c= LeftComp (Cage C,(k + 1))
by A24, XBOOLE_1:1;
then A25:
Ball e,
r misses L~ (Cage C,(k + 1))
by SPRECT_3:43, XBOOLE_1:63;
A26:
(Lower_Appr C) . (k + 1) = Lower_Arc (L~ (Cage C,(k + 1)))
by JORDAN19:def 2;
Lower_Arc (L~ (Cage C,(k + 1))) c= L~ (Cage C,(k + 1))
by JORDAN6:76;
hence
contradiction
by A18, A23, A25, A26, XBOOLE_1:63;
:: thesis: verum end;
end; end;