:: TOPMETR3 semantic presentation

begin

theorem Th1: :: TOPMETR3:1
for X being non empty MetrSpace
for S being sequence of X
for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Element of NAT holds S . n in F ) & F is closed holds
lim S in F
proof
let X be non empty MetrSpace; ::_thesis: for S being sequence of X
for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Element of NAT holds S . n in F ) & F is closed holds
lim S in F
let S be sequence of X; ::_thesis: for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Element of NAT holds S . n in F ) & F is closed holds
lim S in F
let F be Subset of (TopSpaceMetr X); ::_thesis: ( S is convergent & ( for n being Element of NAT holds S . n in F ) & F is closed implies lim S in F )
assume that
A1: S is convergent and
A2: for n being Element of NAT holds S . n in F and
A3: F is closed ; ::_thesis: lim S in F
A4: for G being Subset of (TopSpaceMetr X) st G is open & lim S in G holds
F meets G
proof
let G be Subset of (TopSpaceMetr X); ::_thesis: ( G is open & lim S in G implies F meets G )
assume A5: G is open ; ::_thesis: ( not lim S in G or F meets G )
now__::_thesis:_(_lim_S_in_G_implies_F_meets_G_)
assume  lim S in G ; ::_thesis: F meets G
then consider r1 being real number  such that
A6: r1 > 0 and
A7: Ball ((lim S),r1) c= G by A5, TOPMETR:15;
reconsider r2 = r1 as Real by XREAL_0:def_1;
consider n being Element of NAT  such that
A8: for m being Element of NAT st m >= n holds
dist ((S . m),(lim S)) < r2 by A1, A6, TBSP_1:def_3;
 dist ((S . n),(lim S)) < r2 by A8;
then A9: S . n in Ball ((lim S),r1) by METRIC_1:11;
 S . n in F by A2;
then  S . n in F /\ G by A7, A9, XBOOLE_0:def_4;
hence  F meets G by XBOOLE_0:def_7; ::_thesis: verum
end;
hence  ( not lim S in G or F meets G ) ; ::_thesis: verum
end;
reconsider F0 = F as Subset of (TopSpaceMetr X) ;
 lim S in the carrier of X ;
then  lim S in the carrier of (TopSpaceMetr X) by TOPMETR:12;
then  lim S in Cl F0 by A4, PRE_TOPC:def_7;
hence  lim S in F by A3, PRE_TOPC:22; ::_thesis: verum
end;

theorem Th2: :: TOPMETR3:2
for X, Y being non empty MetrSpace
for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y)
for S being sequence of X holds f * S is sequence of Y
proof
let X, Y be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y)
for S being sequence of X holds f * S is sequence of Y
let f be Function of (TopSpaceMetr X),(TopSpaceMetr Y); ::_thesis: for S being sequence of X holds f * S is sequence of Y
let S be sequence of X; ::_thesis: f * S is sequence of Y
A1: dom f = the carrier of (TopSpaceMetr X) by FUNCT_2:def_1
.= the carrier of X by TOPMETR:12 ;
 ( dom S = NAT & rng S c= the carrier of X ) by FUNCT_2:def_1;
then  dom (f * S) = NAT by A1, RELAT_1:27;
hence  f * S is sequence of Y by FUNCT_2:def_1, TOPMETR:12; ::_thesis: verum
end;

theorem Th3: :: TOPMETR3:3
for X, Y being non empty MetrSpace
for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y)
for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S & f is continuous holds
T is convergent
proof
let X, Y be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y)
for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S & f is continuous holds
T is convergent
let f be Function of (TopSpaceMetr X),(TopSpaceMetr Y); ::_thesis: for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S & f is continuous holds
T is convergent
let S be sequence of X; ::_thesis: for T being sequence of Y st S is convergent & T = f * S & f is continuous holds
T is convergent
let T be sequence of Y; ::_thesis: ( S is convergent & T = f * S & f is continuous implies T is convergent )
assume that
A1: S is convergent and
A2: T = f * S and
A3: f is continuous ; ::_thesis: T is convergent
set z0 = lim S;
reconsider p = lim S as Point of (TopSpaceMetr X) by TOPMETR:12;
A4: dom f = the carrier of (TopSpaceMetr X) by FUNCT_2:def_1
.= the carrier of X by TOPMETR:12 ;
then  f . (lim S) in rng f by FUNCT_1:def_3;
then reconsider x0 = f . (lim S) as Element of Y by TOPMETR:12;
 for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((T . m),x0) < r
proof
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((T . m),x0) < r )
reconsider V = Ball (x0,r) as Subset of (TopSpaceMetr Y) by TOPMETR:12;
assume  r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((T . m),x0) < r
then  ( V is open & x0 in V ) by GOBOARD6:1, TOPMETR:14;
then consider W being Subset of (TopSpaceMetr X) such that
A5: ( p in W & W is open ) and
A6: f .: W c= V by A3, JGRAPH_2:10;
consider r0 being real number  such that
A7: r0 > 0 and
A8: Ball ((lim S),r0) c= W by A5, TOPMETR:15;
reconsider r00 = r0 as Real by XREAL_0:def_1;
consider n0 being Element of NAT  such that
A9: for m being Element of NAT st n0 <= m holds
dist ((S . m),(lim S)) < r00 by A1, A7, TBSP_1:def_3;
 for m being Element of NAT st n0 <= m holds
dist ((T . m),x0) < r
proof
let m be Element of NAT ; ::_thesis: ( n0 <= m implies dist ((T . m),x0) < r )
assume  n0 <= m ; ::_thesis: dist ((T . m),x0) < r
then  dist ((S . m),(lim S)) < r0 by A9;
then  S . m in Ball ((lim S),r0) by METRIC_1:11;
then A10: f . (S . m) in f .: W by A4, A8, FUNCT_1:def_6;
 dom T = NAT by FUNCT_2:def_1;
then  T . m in f .: W by A2, A10, FUNCT_1:12;
hence  dist ((T . m),x0) < r by A6, METRIC_1:11; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((T . m),x0) < r ; ::_thesis: verum
end;
hence  T is convergent by TBSP_1:def_2; ::_thesis: verum
end;

theorem Th4: :: TOPMETR3:4
for s being Real_Sequence
for S being sequence of RealSpace st s = S holds
( ( s is convergent implies S is convergent ) & ( S is convergent implies s is convergent ) & ( s is convergent implies lim s = lim S ) )
proof
let s be Real_Sequence; ::_thesis: for S being sequence of RealSpace st s = S holds
( ( s is convergent implies S is convergent ) & ( S is convergent implies s is convergent ) & ( s is convergent implies lim s = lim S ) )
let S be sequence of RealSpace; ::_thesis: ( s = S implies ( ( s is convergent implies S is convergent ) & ( S is convergent implies s is convergent ) & ( s is convergent implies lim s = lim S ) ) )
assume A1: s = S ; ::_thesis: ( ( s is convergent implies S is convergent ) & ( S is convergent implies s is convergent ) & ( s is convergent implies lim s = lim S ) )
A2: ( s is convergent implies S is convergent )
proof
assume  s is convergent ; ::_thesis: S is convergent
then consider g being real number  such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g) < p by SEQ_2:def_6;
reconsider g0 = g as Real by XREAL_0:def_1;
reconsider x0 = g as Point of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
 for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x0) < r
proof
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x0) < r )
assume  r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x0) < r
then consider n0 being Element of NAT  such that
A4: for m being Element of NAT st n0 <= m holds
abs ((s . m) - g) < r by A3;
 for m being Element of NAT st n0 <= m holds
dist ((S . m),x0) < r
proof
let m be Element of NAT ; ::_thesis: ( n0 <= m implies dist ((S . m),x0) < r )
assume A5: n0 <= m ; ::_thesis: dist ((S . m),x0) < r
reconsider t = s . m as Real ;
dist ((S . m),x0) = real_dist . (t,g) by A1, METRIC_1:def_1, METRIC_1:def_13
.= abs (t - g0) by METRIC_1:def_12 ;
hence  dist ((S . m),x0) < r by A4, A5; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x0) < r ; ::_thesis: verum
end;
hence  S is convergent by TBSP_1:def_2; ::_thesis: verum
end;
 ( S is convergent implies s is convergent )
proof
assume  S is convergent ; ::_thesis: s is convergent
then consider x being Element of RealSpace such that
A6: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x) < r by TBSP_1:def_2;
reconsider g0 = x as Real by METRIC_1:def_13;
 for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g0) < p
proof
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g0) < p )
reconsider p0 = p as Real by XREAL_0:def_1;
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g0) < p
then consider n0 being Element of NAT  such that
A7: for m being Element of NAT st n0 <= m holds
dist ((S . m),x) < p0 by A6;
 for m being Element of NAT st n0 <= m holds
abs ((s . m) - g0) < p
proof
let m be Element of NAT ; ::_thesis: ( n0 <= m implies abs ((s . m) - g0) < p )
assume A8: n0 <= m ; ::_thesis: abs ((s . m) - g0) < p
reconsider t = s . m as Real ;
dist ((S . m),x) = real_dist . (t,g0) by A1, METRIC_1:def_1, METRIC_1:def_13
.= abs (t - g0) by METRIC_1:def_12 ;
hence  abs ((s . m) - g0) < p by A7, A8; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g0) < p ; ::_thesis: verum
end;
hence  s is convergent by SEQ_2:def_6; ::_thesis: verum
end;
hence  ( s is convergent iff S is convergent ) by A2; ::_thesis: ( s is convergent implies lim s = lim S )
thus  ( s is convergent implies lim s = lim S ) ::_thesis: verum
proof
reconsider g0 = lim S as Real by METRIC_1:def_13;
assume A9: s is convergent ; ::_thesis: lim s = lim S
 for r being real number st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - g0) < r
proof
let r be real number ; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - g0) < r )
reconsider r0 = r as Real by XREAL_0:def_1;
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - g0) < r
then consider m0 being Element of NAT  such that
A10: for n being Element of NAT st m0 <= n holds
dist ((S . n),(lim S)) < r0 by A2, A9, TBSP_1:def_3;
 for n being Element of NAT st m0 <= n holds
abs ((s . n) - g0) < r
proof
let n be Element of NAT ; ::_thesis: ( m0 <= n implies abs ((s . n) - g0) < r )
assume A11: m0 <= n ; ::_thesis: abs ((s . n) - g0) < r
dist ((S . n),(lim S)) = real_dist . ((s . n),g0) by A1, METRIC_1:def_1, METRIC_1:def_13
.= abs ((s . n) - g0) by METRIC_1:def_12 ;
hence  abs ((s . n) - g0) < r by A10, A11; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - g0) < r ; ::_thesis: verum
end;
hence  lim s = lim S by A9, SEQ_2:def_7; ::_thesis: verum
end;
end;

theorem Th5: :: TOPMETR3:5
for a, b being real number
for s being Real_Sequence st rng s c= [.a,b.] holds
s is sequence of (Closed-Interval-MSpace (a,b))
proof
let a, b be real number ; ::_thesis: for s being Real_Sequence st rng s c= [.a,b.] holds
s is sequence of (Closed-Interval-MSpace (a,b))
let s be Real_Sequence; ::_thesis: ( rng s c= [.a,b.] implies s is sequence of (Closed-Interval-MSpace (a,b)) )
assume A1: rng s c= [.a,b.] ; ::_thesis: s is sequence of (Closed-Interval-MSpace (a,b))
reconsider t = s . 0 as Real ;
A2: dom s = NAT by FUNCT_2:def_1;
then  s . 0 in rng s by FUNCT_1:def_3;
then  ( a <= t & t <= b ) by A1, XXREAL_1:1;
then  the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by TOPMETR:10, XXREAL_0:2;
hence  s is sequence of (Closed-Interval-MSpace (a,b)) by A1, A2, FUNCT_2:2; ::_thesis: verum
end;

theorem Th6: :: TOPMETR3:6
for a, b being real number
for S being sequence of (Closed-Interval-MSpace (a,b)) st a <= b holds
S is sequence of RealSpace
proof
let a, b be real number ; ::_thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st a <= b holds
S is sequence of RealSpace
let S be sequence of (Closed-Interval-MSpace (a,b)); ::_thesis: ( a <= b implies S is sequence of RealSpace )
assume  a <= b ; ::_thesis: S is sequence of RealSpace
then  the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by TOPMETR:10;
then  ( dom S = NAT & rng S c= the carrier of RealSpace ) by FUNCT_2:def_1, METRIC_1:def_13, XBOOLE_1:1;
hence  S is sequence of RealSpace by FUNCT_2:2; ::_thesis: verum
end;

theorem Th7: :: TOPMETR3:7
for a, b being real number
for S1 being sequence of (Closed-Interval-MSpace (a,b))
for S being sequence of RealSpace st S = S1 & a <= b holds
( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )
proof
let a, b be real number ; ::_thesis: for S1 being sequence of (Closed-Interval-MSpace (a,b))
for S being sequence of RealSpace st S = S1 & a <= b holds
( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )
let S1 be sequence of (Closed-Interval-MSpace (a,b)); ::_thesis: for S being sequence of RealSpace st S = S1 & a <= b holds
( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )
let S be sequence of RealSpace; ::_thesis: ( S = S1 & a <= b implies ( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) ) )
assume that
A1: S = S1 and
A2: a <= b ; ::_thesis: ( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )
reconsider P = [.a,b.] as Subset of R^1 by TOPMETR:17;
A3: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A2, TOPMETR:10;
A4: ( S is convergent implies S1 is convergent )
proof
A5: for m being Element of NAT holds S . m in [.a,b.]
proof
let m be Element of NAT ; ::_thesis: S . m in [.a,b.]
 dom S1 = NAT by FUNCT_2:def_1;
then  S1 . m in rng S1 by FUNCT_1:def_3;
hence  S . m in [.a,b.] by A1, A3; ::_thesis: verum
end;
A6: P is closed by TREAL_1:1;
assume A7: S is convergent ; ::_thesis: S1 is convergent
then consider x0 being Element of RealSpace such that
A8: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x0) < r by TBSP_1:def_2;
 x0 = lim S by A7, A8, TBSP_1:def_3;
then reconsider x1 = x0 as Element of (Closed-Interval-MSpace (a,b)) by A3, A7, A5, A6, Th1, TOPMETR:def_6;
 for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S1 . m),x1) < r
proof
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S1 . m),x1) < r )
assume  r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S1 . m),x1) < r
then consider n0 being Element of NAT  such that
A9: for m being Element of NAT st n0 <= m holds
dist ((S . m),x0) < r by A8;
 for m being Element of NAT st n0 <= m holds
dist ((S1 . m),x1) < r
proof
let m be Element of NAT ; ::_thesis: ( n0 <= m implies dist ((S1 . m),x1) < r )
assume A10: n0 <= m ; ::_thesis: dist ((S1 . m),x1) < r
dist ((S1 . m),x1) = the distance of (Closed-Interval-MSpace (a,b)) . ((S1 . m),x1) by METRIC_1:def_1
.= the distance of RealSpace . ((S1 . m),x1) by TOPMETR:def_1
.= dist ((S . m),x0) by A1, METRIC_1:def_1 ;
hence  dist ((S1 . m),x1) < r by A9, A10; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S1 . m),x1) < r ; ::_thesis: verum
end;
hence  S1 is convergent by TBSP_1:def_2; ::_thesis: verum
end;
 ( S1 is convergent implies S is convergent )
proof
assume  S1 is convergent ; ::_thesis: S is convergent
then consider x0 being Element of (Closed-Interval-MSpace (a,b)) such that
A11: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S1 . m),x0) < r by TBSP_1:def_2;
 x0 in [.a,b.] by A3;
then reconsider x1 = x0 as Element of RealSpace by METRIC_1:def_13;
 for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x1) < r
proof
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x1) < r )
assume  r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x1) < r
then consider n0 being Element of NAT  such that
A12: for m being Element of NAT st n0 <= m holds
dist ((S1 . m),x0) < r by A11;
 for m being Element of NAT st n0 <= m holds
dist ((S . m),x1) < r
proof
let m be Element of NAT ; ::_thesis: ( n0 <= m implies dist ((S . m),x1) < r )
assume A13: n0 <= m ; ::_thesis: dist ((S . m),x1) < r
dist ((S1 . m),x0) = the distance of (Closed-Interval-MSpace (a,b)) . ((S1 . m),x0) by METRIC_1:def_1
.= the distance of RealSpace . ((S1 . m),x0) by TOPMETR:def_1
.= dist ((S . m),x1) by A1, METRIC_1:def_1 ;
hence  dist ((S . m),x1) < r by A12, A13; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x1) < r ; ::_thesis: verum
end;
hence  S is convergent by TBSP_1:def_2; ::_thesis: verum
end;
hence  ( S is convergent iff S1 is convergent ) by A4; ::_thesis: ( S is convergent implies lim S = lim S1 )
thus  ( S is convergent implies lim S = lim S1 ) ::_thesis: verum
proof
 lim S1 in the carrier of (Closed-Interval-MSpace (a,b)) ;
then reconsider t0 = lim S1 as Point of RealSpace by A3, METRIC_1:def_13;
assume A14: S is convergent ; ::_thesis: lim S = lim S1
 for r1 being Real st 0 < r1 holds
ex m1 being Element of NAT st
for n1 being Element of NAT st m1 <= n1 holds
dist ((S . n1),t0) < r1
proof
let r1 be Real; ::_thesis: ( 0 < r1 implies ex m1 being Element of NAT st
for n1 being Element of NAT st m1 <= n1 holds
dist ((S . n1),t0) < r1 )
assume  0 < r1 ; ::_thesis: ex m1 being Element of NAT st
for n1 being Element of NAT st m1 <= n1 holds
dist ((S . n1),t0) < r1
then consider m1 being Element of NAT  such that
A15: for n1 being Element of NAT st m1 <= n1 holds
dist ((S1 . n1),(lim S1)) < r1 by A4, A14, TBSP_1:def_3;
 for n1 being Element of NAT st m1 <= n1 holds
dist ((S . n1),t0) < r1
proof
let n1 be Element of NAT ; ::_thesis: ( m1 <= n1 implies dist ((S . n1),t0) < r1 )
assume A16: m1 <= n1 ; ::_thesis: dist ((S . n1),t0) < r1
dist ((S1 . n1),(lim S1)) = the distance of (Closed-Interval-MSpace (a,b)) . ((S1 . n1),(lim S1)) by METRIC_1:def_1
.= the distance of RealSpace . ((S1 . n1),(lim S1)) by TOPMETR:def_1
.= dist ((S . n1),t0) by A1, METRIC_1:def_1 ;
hence  dist ((S . n1),t0) < r1 by A15, A16; ::_thesis: verum
end;
hence  ex m1 being Element of NAT st
for n1 being Element of NAT st m1 <= n1 holds
dist ((S . n1),t0) < r1 ; ::_thesis: verum
end;
hence  lim S = lim S1 by A14, TBSP_1:def_3; ::_thesis: verum
end;
end;

theorem Th8: :: TOPMETR3:8
for a, b being real number
for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is convergent holds
( S is convergent & lim s = lim S )
proof
let a, b be real number ; ::_thesis: for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is convergent holds
( S is convergent & lim s = lim S )
let s be Real_Sequence; ::_thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is convergent holds
( S is convergent & lim s = lim S )
let S be sequence of (Closed-Interval-MSpace (a,b)); ::_thesis: ( S = s & a <= b & s is convergent implies ( S is convergent & lim s = lim S ) )
assume that
A1: S = s and
A2: a <= b and
A3: s is convergent ; ::_thesis: ( S is convergent & lim s = lim S )
reconsider S0 = S as sequence of RealSpace by A2, Th6;
A4: S0 is convergent by A1, A3, Th4;
hence  S is convergent by A2, Th7; ::_thesis: lim s = lim S
 lim S0 = lim S by A2, A4, Th7;
hence  lim s = lim S by A1, A3, Th4; ::_thesis: verum
end;

theorem :: TOPMETR3:9
for a, b being real number
for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-decreasing holds
S is convergent
proof
let a, b be real number ; ::_thesis: for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-decreasing holds
S is convergent
let s be Real_Sequence; ::_thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-decreasing holds
S is convergent
let S be sequence of (Closed-Interval-MSpace (a,b)); ::_thesis: ( S = s & a <= b & s is non-decreasing implies S is convergent )
assume that
A1: S = s and
A2: a <= b and
A3: s is non-decreasing ; ::_thesis: S is convergent
 for n being Element of NAT holds s . n < b + 1
proof
let n be Element of NAT ; ::_thesis: s . n < b + 1
A4: b < b + 1 by XREAL_1:29;
 dom S = NAT by FUNCT_2:def_1;
then A5: s . n in rng S by A1, FUNCT_1:def_3;
 the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A2, TOPMETR:10;
then  s . n <= b by A5, XXREAL_1:1;
hence  s . n < b + 1 by A4, XXREAL_0:2; ::_thesis: verum
end;
then  s is bounded_above by SEQ_2:def_3;
hence  S is convergent by A1, A2, A3, Th8; ::_thesis: verum
end;

theorem :: TOPMETR3:10
for a, b being real number
for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds
S is convergent
proof
let a, b be real number ; ::_thesis: for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds
S is convergent
let s be Real_Sequence; ::_thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds
S is convergent
let S be sequence of (Closed-Interval-MSpace (a,b)); ::_thesis: ( S = s & a <= b & s is non-increasing implies S is convergent )
assume that
A1: S = s and
A2: a <= b and
A3: s is non-increasing ; ::_thesis: S is convergent
 for n being Element of NAT holds s . n > a - 1
proof
let n be Element of NAT ; ::_thesis: s . n > a - 1
 a < a + 1 by XREAL_1:29;
then A4: a - 1 < a by XREAL_1:19;
 dom S = NAT by FUNCT_2:def_1;
then A5: s . n in rng S by A1, FUNCT_1:def_3;
 the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A2, TOPMETR:10;
then  a <= s . n by A5, XXREAL_1:1;
hence  s . n > a - 1 by A4, XXREAL_0:2; ::_thesis: verum
end;
then  s is bounded_below by SEQ_2:def_4;
hence  S is convergent by A1, A2, A3, Th8; ::_thesis: verum
end;

theorem Th11: :: TOPMETR3:11
for R being non empty Subset of REAL st R is bounded_above holds
ex s being Real_Sequence st
( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R )
proof
let R be non empty Subset of REAL; ::_thesis: ( R is bounded_above implies ex s being Real_Sequence st
( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R ) )
reconsider rs = upper_bound R as real number ;
defpred S1[ Element of NAT , real number ] means ( $2 in R & ( for r00 being real number st r00 = $2 holds
rs - (1 / ($1 + 1)) < r00 ) );
assume A1: R is bounded_above ; ::_thesis: ex s being Real_Sequence st
( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R )
A2: for n being Element of NAT ex r being Real st S1[n,r]
proof
let n be Element of NAT ; ::_thesis: ex r being Real st S1[n,r]
 (n + 1) " > 0 ;
then  1 / (n + 1) > 0 by XCMPLX_1:215;
then consider r0 being real number  such that
A3: r0 in R and
A4: rs - (1 / (n + 1)) < r0 by A1, SEQ_4:def_1;
 for r00 being real number st r00 = r0 holds
rs - (1 / (n + 1)) < r00 by A4;
hence  ex r being Real st S1[n,r] by A3; ::_thesis: verum
end;
 ex s1 being Function of NAT,REAL st
for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A2);
then consider s1 being Function of NAT,REAL such that
A5: for n being Element of NAT holds
( s1 . n in R & ( for r0 being real number st r0 = s1 . n holds
rs - (1 / (n + 1)) < r0 ) ) ;
defpred S2[ set , set , set ] means ( ( $2 is real number implies for r1, r2 being real number
for n1 being Nat st r1 = $2 & r2 = s1 . (n1 + 1) & n1 = $1 holds
( ( r1 >= r2 implies $3 = $2 ) & ( r1 < r2 implies $3 = s1 . (n1 + 1) ) ) ) & ( $2 is not real number implies $3 = 1 ) );
A6: for n being Element of NAT
for x being set ex y being set st S2[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S2[n,x,y]
thus  for x being set ex y being set st S2[n,x,y] ::_thesis: verum
proof
let x be set ; ::_thesis: ex y being set st S2[n,x,y]
now__::_thesis:_(_(_x_is_not_real_number_&_ex_y_being_set_st_S2[n,x,y]_)_or_(_x_is_real_number_&_ex_y_being_set_st_S2[n,x,y]_)_)
percases ( not x is real number or x is real number ) ;
case x is not real number ; ::_thesis: ex y being set st S2[n,x,y]
hence  ex y being set st S2[n,x,y] ; ::_thesis: verum
end;
caseA7: x is real number ; ::_thesis: ex y being set st S2[n,x,y]
then reconsider r10 = x as real number ;
reconsider r20 = s1 . (n + 1) as real number ;
now__::_thesis:_(_(_r10_>=_r20_&_ex_y_being_set_st_S2[n,x,y]_)_or_(_r10_<_r20_&_ex_y_being_set_st_S2[n,x,y]_)_)
percases ( r10 >= r20 or r10 < r20 ) ;
case r10 >= r20 ; ::_thesis: ex y being set st S2[n,x,y]
then  for r1, r2 being real number
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 >= r2 implies x = x ) & ( r1 < r2 implies x = s1 . (n1 + 1) ) ) ;
hence  ex y being set st S2[n,x,y] by A7; ::_thesis: verum
end;
case r10 < r20 ; ::_thesis: ex y being set st S2[n,x,y]
then  for r1, r2 being real number
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 >= r2 implies s1 . (n + 1) = x ) & ( r1 < r2 implies s1 . (n + 1) = s1 . (n1 + 1) ) ) ;
hence  ex y being set st S2[n,x,y] by A7; ::_thesis: verum
end;
end;
end;
hence  ex y being set st S2[n,x,y] ; ::_thesis: verum
end;
end;
end;
hence  ex y being set st S2[n,x,y] ; ::_thesis: verum
end;
end;
 ex f being Function st
( dom f = NAT & f . 0 = s1 . 0 & ( for n being Element of NAT holds S2[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_1(A6);
then consider s2 being Function such that
A8: dom s2 = NAT and
A9: s2 . 0 = s1 . 0 and
A10: for n being Element of NAT holds S2[n,s2 . n,s2 . (n + 1)] ;
A11: rng s2 c= REAL
proof
defpred S3[ Nat] means s2 . $1 in REAL ;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s2 or y in REAL )
assume  y in rng s2 ; ::_thesis: y in REAL
then consider x being set  such that
A12: x in dom s2 and
A13: y = s2 . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A8, A12;
A14: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
reconsider r2 = s1 . (k + 1) as Real ;
assume A15: s2 . k in REAL ; ::_thesis: S3[k + 1]
then reconsider r1 = s2 . k as Real ;
now__::_thesis:_(_(_r1_>=_r2_&_S3[k_+_1]_)_or_(_r1_<_r2_&_S3[k_+_1]_)_)
percases ( r1 >= r2 or r1 < r2 ) ;
case r1 >= r2 ; ::_thesis: S3[k + 1]
hence  S3[k + 1] by A10, A15; ::_thesis: verum
end;
case r1 < r2 ; ::_thesis: S3[k + 1]
then  s2 . (k + 1) = s1 . (k + 1) by A10;
hence  S3[k + 1] ; ::_thesis: verum
end;
end;
end;
hence  S3[k + 1] ; ::_thesis: verum
end;
A16: S3[ 0 ] by A9;
 for m being Element of NAT holds S3[m] from NAT_1:sch_1(A16, A14);
then  s2 . n in REAL ;
hence  y in REAL by A13; ::_thesis: verum
end;
then reconsider s3 = s2 as Real_Sequence by A8, FUNCT_2:2;
defpred S3[ Nat] means s1 . $1 <= s3 . $1;
A17: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume  s1 . k <= s3 . k ; ::_thesis: S3[k + 1]
reconsider r2 = s1 . (k + 1) as real number ;
 s2 . k in rng s2 by A8, FUNCT_1:def_3;
then reconsider r1 = s2 . k as real number by A11;
now__::_thesis:_(_(_r1_>=_r2_&_S3[k_+_1]_)_or_(_r1_<_r2_&_S3[k_+_1]_)_)
percases ( r1 >= r2 or r1 < r2 ) ;
case r1 >= r2 ; ::_thesis: S3[k + 1]
hence  S3[k + 1] by A10; ::_thesis: verum
end;
case r1 < r2 ; ::_thesis: S3[k + 1]
hence  S3[k + 1] by A10; ::_thesis: verum
end;
end;
end;
hence  S3[k + 1] ; ::_thesis: verum
end;
A18: S3[ 0 ] by A9;
A19: for n4 being Element of NAT holds S3[n4] from NAT_1:sch_1(A18, A17);
defpred S4[ Nat] means ( 0 <= $1 implies s3 . 0 <= s3 . $1 );
A20: for n4 being Element of NAT holds s3 . n4 <= s3 . (n4 + 1)
proof
let n4 be Element of NAT ; ::_thesis: s3 . n4 <= s3 . (n4 + 1)
reconsider r2 = s1 . (n4 + 1) as real number ;
 dom s3 = NAT by FUNCT_2:def_1;
then reconsider r1 = s2 . n4 as real number ;
now__::_thesis:_(_(_r1_>=_r2_&_s3_._n4_<=_s3_._(n4_+_1)_)_or_(_r1_<_r2_&_s3_._n4_<=_s3_._(n4_+_1)_)_)
percases ( r1 >= r2 or r1 < r2 ) ;
case r1 >= r2 ; ::_thesis: s3 . n4 <= s3 . (n4 + 1)
hence  s3 . n4 <= s3 . (n4 + 1) by A10; ::_thesis: verum
end;
case r1 < r2 ; ::_thesis: s3 . n4 <= s3 . (n4 + 1)
hence  s3 . n4 <= s3 . (n4 + 1) by A10; ::_thesis: verum
end;
end;
end;
hence  s3 . n4 <= s3 . (n4 + 1) ; ::_thesis: verum
end;
A21: for k being Element of NAT st S4[k] holds
S4[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] )
assume A22: ( 0 <= k implies s3 . 0 <= s3 . k ) ; ::_thesis: S4[k + 1]
now__::_thesis:_(_0_<=_k_+_1_implies_s3_._0_<=_s3_._(k_+_1)_)
assume  0 <= k + 1 ; ::_thesis: s3 . 0 <= s3 . (k + 1)
A23: s3 . k <= s3 . (k + 1) by A20;
now__::_thesis:_(_(_0_<_k_&_s3_._0_<=_s3_._(k_+_1)_)_or_(_0_=_k_&_s3_._0_<=_s3_._(k_+_1)_)_)
percases ( 0 < k or 0 = k ) ;
case 0 < k ; ::_thesis: s3 . 0 <= s3 . (k + 1)
thus  s3 . 0 <= s3 . (k + 1) by A22, A23, XXREAL_0:2; ::_thesis: verum
end;
case 0 = k ; ::_thesis: s3 . 0 <= s3 . (k + 1)
hence  s3 . 0 <= s3 . (k + 1) by A20; ::_thesis: verum
end;
end;
end;
hence  s3 . 0 <= s3 . (k + 1) ; ::_thesis: verum
end;
hence  S4[k + 1] ; ::_thesis: verum
end;
defpred S5[ Nat] means  for n4 being Element of NAT st $1 <= n4 holds
s3 . $1 <= s3 . n4;
A24: for k being Element of NAT st S5[k] holds
S5[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S5[k] implies S5[k + 1] )
assume  for n5 being Element of NAT st k <= n5 holds
s3 . k <= s3 . n5 ; ::_thesis: S5[k + 1]
defpred S6[ Nat] means ( k + 1 <= $1 implies s3 . (k + 1) <= s3 . $1 );
A25: for i being Element of NAT st S6[i] holds
S6[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S6[i] implies S6[i + 1] )
reconsider r2 = s1 . (i + 1) as real number ;
 s2 . i in rng s2 by A8, FUNCT_1:def_3;
then reconsider r1 = s2 . i as real number by A11;
A26: now__::_thesis:_(_(_r1_>=_r2_&_s3_._i_<=_s3_._(i_+_1)_)_or_(_r1_<_r2_&_s3_._i_<=_s3_._(i_+_1)_)_)
percases ( r1 >= r2 or r1 < r2 ) ;
case r1 >= r2 ; ::_thesis: s3 . i <= s3 . (i + 1)
hence  s3 . i <= s3 . (i + 1) by A10; ::_thesis: verum
end;
case r1 < r2 ; ::_thesis: s3 . i <= s3 . (i + 1)
hence  s3 . i <= s3 . (i + 1) by A10; ::_thesis: verum
end;
end;
end;
assume A27: ( k + 1 <= i implies s3 . (k + 1) <= s3 . i ) ; ::_thesis: S6[i + 1]
now__::_thesis:_(_k_+_1_<=_i_+_1_implies_s3_._(k_+_1)_<=_s3_._(i_+_1)_)
assume A28: k + 1 <= i + 1 ; ::_thesis: s3 . (k + 1) <= s3 . (i + 1)
now__::_thesis:_(_(_k_+_1_<_i_+_1_&_s3_._(k_+_1)_<=_s3_._(i_+_1)_)_or_(_k_+_1_=_i_+_1_&_s3_._(k_+_1)_<=_s3_._(i_+_1)_)_)
percases ( k + 1 < i + 1 or k + 1 = i + 1 ) by A28, XXREAL_0:1;
case k + 1 < i + 1 ; ::_thesis: s3 . (k + 1) <= s3 . (i + 1)
hence  s3 . (k + 1) <= s3 . (i + 1) by A27, A26, NAT_1:13, XXREAL_0:2; ::_thesis: verum
end;
case k + 1 = i + 1 ; ::_thesis: s3 . (k + 1) <= s3 . (i + 1)
hence  s3 . (k + 1) <= s3 . (i + 1) ; ::_thesis: verum
end;
end;
end;
hence  s3 . (k + 1) <= s3 . (i + 1) ; ::_thesis: verum
end;
hence  S6[i + 1] ; ::_thesis: verum
end;
A29: S6[ 0 ] ;
 for n4 being Element of NAT holds S6[n4] from NAT_1:sch_1(A29, A25);
hence  S5[k + 1] ; ::_thesis: verum
end;
A30: S4[ 0 ] ;
 for n4 being Element of NAT holds S4[n4] from NAT_1:sch_1(A30, A21);
then A31: S5[ 0 ] ;
 for m4 being Element of NAT holds S5[m4] from NAT_1:sch_1(A31, A24);
then  for m4, n4 being Element of NAT st m4 in dom s3 & n4 in dom s3 & m4 <= n4 holds
s3 . m4 <= s3 . n4 ;
then A32: s3 is non-decreasing by SEQM_3:def_3;
A33: rng s3 c= R
proof
defpred S6[ set ] means s3 . $1 in R;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s3 or y in R )
assume  y in rng s3 ; ::_thesis: y in R
then A34: ex x being set st
( x in dom s3 & y = s3 . x ) by FUNCT_1:def_3;
A35: for k being Element of NAT st S6[k] holds
S6[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S6[k] implies S6[k + 1] )
reconsider r2 = s1 . (k + 1) as real number ;
 s2 . k in rng s2 by A8, FUNCT_1:def_3;
then reconsider r1 = s2 . k as real number by A11;
assume A36: s3 . k in R ; ::_thesis: S6[k + 1]
now__::_thesis:_(_(_r1_>=_r2_&_S6[k_+_1]_)_or_(_r1_<_r2_&_S6[k_+_1]_)_)
percases ( r1 >= r2 or r1 < r2 ) ;
case r1 >= r2 ; ::_thesis: S6[k + 1]
hence  S6[k + 1] by A10, A36; ::_thesis: verum
end;
case r1 < r2 ; ::_thesis: S6[k + 1]
then  s2 . (k + 1) = s1 . (k + 1) by A10;
hence  S6[k + 1] by A5; ::_thesis: verum
end;
end;
end;
hence  S6[k + 1] ; ::_thesis: verum
end;
A37: S6[ 0 ] by A5, A9;
 for nn being Element of NAT holds S6[nn] from NAT_1:sch_1(A37, A35);
hence  y in R by A34; ::_thesis: verum
end;
 for n being Element of NAT holds s3 . n < (upper_bound R) + 1
proof
let n be Element of NAT ; ::_thesis: s3 . n < (upper_bound R) + 1
 s3 . n in rng s3 by A8, FUNCT_1:def_3;
then A38: s3 . n <= upper_bound R by A1, A33, SEQ_4:def_1;
 upper_bound R < (upper_bound R) + 1 by XREAL_1:29;
hence  s3 . n < (upper_bound R) + 1 by A38, XXREAL_0:2; ::_thesis: verum
end;
then A39: s3 is bounded_above by SEQ_2:def_3;
A40: for r being Real st r > 0 holds
(upper_bound R) - r < lim s3
proof
let r be Real; ::_thesis: ( r > 0 implies (upper_bound R) - r < lim s3 )
assume A41: r > 0 ; ::_thesis: (upper_bound R) - r < lim s3
consider n2 being Element of NAT  such that
A42: 1 / r < n2 by SEQ_4:3;
 n2 < n2 + 1 by XREAL_1:29;
then  1 / r < n2 + 1 by A42, XXREAL_0:2;
then  (1 / r) * r < (n2 + 1) * r by A41, XREAL_1:68;
then  1 < (n2 + 1) * r by A41, XCMPLX_1:106;
then  1 / (n2 + 1) < ((n2 + 1) * r) / (n2 + 1) by XREAL_1:74;
then  1 / (n2 + 1) < r by XCMPLX_1:89;
then  rs - (1 / (n2 + 1)) > rs - r by XREAL_1:10;
then A43: rs - r < s1 . n2 by A5, XXREAL_0:2;
A44: s3 . n2 <= lim s3 by A32, A39, SEQ_4:37;
 s1 . n2 <= s3 . n2 by A19;
then  rs - r < s3 . n2 by A43, XXREAL_0:2;
hence  (upper_bound R) - r < lim s3 by A44, XXREAL_0:2; ::_thesis: verum
end;
A45: now__::_thesis:_not_upper_bound_R_>_lim_s3
reconsider r = (upper_bound R) - (lim s3) as Real ;
assume  upper_bound R > lim s3 ; ::_thesis: contradiction
then  r > 0 by XREAL_1:50;
then  (upper_bound R) - r < lim s3 by A40;
hence  contradiction ; ::_thesis: verum
end;
A46: for n being Element of NAT holds s3 . n <= upper_bound R
proof
let n be Element of NAT ; ::_thesis: s3 . n <= upper_bound R
 dom s3 = NAT by FUNCT_2:def_1;
then  s3 . n in rng s3 by FUNCT_1:def_3;
hence  s3 . n <= upper_bound R by A1, A33, SEQ_4:def_1; ::_thesis: verum
end;
 for n being Element of NAT holds s3 . n < (upper_bound R) + 1
proof
let n be Element of NAT ; ::_thesis: s3 . n < (upper_bound R) + 1
 ( upper_bound R < (upper_bound R) + 1 & s3 . n <= upper_bound R ) by A46, XREAL_1:29;
hence  s3 . n < (upper_bound R) + 1 by XXREAL_0:2; ::_thesis: verum
end;
then A47: s3 is bounded_above by SEQ_2:def_3;
then  lim s3 <= upper_bound R by A32, A46, PREPOWER:2;
hence  ex s being Real_Sequence st
( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R ) by A32, A33, A47, A45, XXREAL_0:1; ::_thesis: verum
end;

theorem Th12: :: TOPMETR3:12
for R being non empty Subset of REAL st R is bounded_below holds
ex s being Real_Sequence st
( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R )
proof
let R be non empty Subset of REAL; ::_thesis: ( R is bounded_below implies ex s being Real_Sequence st
( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R ) )
reconsider rs = lower_bound R as real number ;
defpred S1[ Element of NAT , real number ] means ( $2 in R & ( for r00 being real number st r00 = $2 holds
rs + (1 / ($1 + 1)) > r00 ) );
assume A1: R is bounded_below ; ::_thesis: ex s being Real_Sequence st
( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R )
A2: for n being Element of NAT ex r being Real st S1[n,r]
proof
let n be Element of NAT ; ::_thesis: ex r being Real st S1[n,r]
 (n + 1) " > 0 ;
then  1 / (n + 1) > 0 by XCMPLX_1:215;
then consider r0 being real number  such that
A3: r0 in R and
A4: rs + (1 / (n + 1)) > r0 by A1, SEQ_4:def_2;
 for r00 being real number st r00 = r0 holds
rs + (1 / (n + 1)) > r00 by A4;
hence  ex r being Real st S1[n,r] by A3; ::_thesis: verum
end;
 ex s1 being Function of NAT,REAL st
for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A2);
then consider s1 being Function of NAT,REAL such that
A5: for n being Element of NAT holds
( s1 . n in R & ( for r0 being real number st r0 = s1 . n holds
rs + (1 / (n + 1)) > r0 ) ) ;
defpred S2[ set , set , set ] means ( ( $2 is real number implies for r1, r2 being real number
for n1 being Nat st r1 = $2 & r2 = s1 . (n1 + 1) & n1 = $1 holds
( ( r1 <= r2 implies $3 = $2 ) & ( r1 > r2 implies $3 = s1 . (n1 + 1) ) ) ) & ( $2 is not real number implies $3 = 1 ) );
A6: for n being Element of NAT
for x being set ex y being set st S2[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S2[n,x,y]
thus  for x being set ex y being set st S2[n,x,y] ::_thesis: verum
proof
let x be set ; ::_thesis: ex y being set st S2[n,x,y]
now__::_thesis:_(_(_x_is_not_real_number_&_ex_y_being_set_st_
(_(_x_is_real_number_implies_for_r1,_r2_being_real_number_
for_n1_being_Nat_st_r1_=_x_&_r2_=_s1_._(n1_+_1)_&_n1_=_n_holds_
(_(_r1_>=_r2_implies_y_=_x_)_&_(_r1_<_r2_implies_y_=_s1_._(n1_+_1)_)_)_)_&_(_x_is_not_real_number_implies_y_=_1_)_)_)_or_(_x_is_real_number_&_ex_y_being_set_st_S2[n,x,y]_)_)
percases ( not x is real number or x is real number ) ;
case x is not real number ; ::_thesis: ex y being set st
( ( x is real number implies for r1, r2 being real number
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 >= r2 implies y = x ) & ( r1 < r2 implies y = s1 . (n1 + 1) ) ) ) & ( x is not real number implies y = 1 ) )
hence  ex y being set st
( ( x is real number implies for r1, r2 being real number
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 >= r2 implies y = x ) & ( r1 < r2 implies y = s1 . (n1 + 1) ) ) ) & ( x is not real number implies y = 1 ) ) ; ::_thesis: verum
end;
caseA7: x is real number ; ::_thesis: ex y being set st S2[n,x,y]
then reconsider r10 = x as real number ;
reconsider r20 = s1 . (n + 1) as real number ;
now__::_thesis:_(_(_r10_<=_r20_&_ex_y_being_set_st_S2[n,x,y]_)_or_(_r10_>_r20_&_ex_y_being_set_st_S2[n,x,y]_)_)
percases ( r10 <= r20 or r10 > r20 ) ;
case r10 <= r20 ; ::_thesis: ex y being set st S2[n,x,y]
then  for r1, r2 being real number
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 <= r2 implies x = x ) & ( r1 > r2 implies x = s1 . (n1 + 1) ) ) ;
hence  ex y being set st S2[n,x,y] by A7; ::_thesis: verum
end;
case r10 > r20 ; ::_thesis: ex y being set st S2[n,x,y]
then  for r1, r2 being real number
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 <= r2 implies s1 . (n + 1) = x ) & ( r1 > r2 implies s1 . (n + 1) = s1 . (n1 + 1) ) ) ;
hence  ex y being set st S2[n,x,y] by A7; ::_thesis: verum
end;
end;
end;
hence  ex y being set st S2[n,x,y] ; ::_thesis: verum
end;
end;
end;
hence  ex y being set st S2[n,x,y] ; ::_thesis: verum
end;
end;
 ex f being Function st
( dom f = NAT & f . 0 = s1 . 0 & ( for n being Element of NAT holds S2[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_1(A6);
then consider s2 being Function such that
A8: dom s2 = NAT and
A9: s2 . 0 = s1 . 0 and
A10: for n being Element of NAT holds S2[n,s2 . n,s2 . (n + 1)] ;
A11: rng s2 c= REAL
proof
defpred S3[ Nat] means s2 . $1 in REAL ;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s2 or y in REAL )
assume  y in rng s2 ; ::_thesis: y in REAL
then consider x being set  such that
A12: x in dom s2 and
A13: y = s2 . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A8, A12;
A14: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
reconsider r2 = s1 . (k + 1) as Real ;
assume A15: s2 . k in REAL ; ::_thesis: S3[k + 1]
then reconsider r1 = s2 . k as Real ;
now__::_thesis:_(_(_r1_<=_r2_&_S3[k_+_1]_)_or_(_r1_>_r2_&_S3[k_+_1]_)_)
percases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; ::_thesis: S3[k + 1]
hence  S3[k + 1] by A10, A15; ::_thesis: verum
end;
case r1 > r2 ; ::_thesis: S3[k + 1]
then  s2 . (k + 1) = s1 . (k + 1) by A10;
hence  S3[k + 1] ; ::_thesis: verum
end;
end;
end;
hence  S3[k + 1] ; ::_thesis: verum
end;
A16: S3[ 0 ] by A9;
 for m being Element of NAT holds S3[m] from NAT_1:sch_1(A16, A14);
then  s2 . n in REAL ;
hence  y in REAL by A13; ::_thesis: verum
end;
then reconsider s3 = s2 as Real_Sequence by A8, FUNCT_2:2;
defpred S3[ Nat] means s1 . $1 >= s3 . $1;
A17: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume  s1 . k >= s3 . k ; ::_thesis: S3[k + 1]
reconsider r2 = s1 . (k + 1) as real number ;
 s2 . k in rng s2 by A8, FUNCT_1:def_3;
then reconsider r1 = s2 . k as real number by A11;
now__::_thesis:_(_(_r1_<=_r2_&_S3[k_+_1]_)_or_(_r1_>_r2_&_S3[k_+_1]_)_)
percases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; ::_thesis: S3[k + 1]
hence  S3[k + 1] by A10; ::_thesis: verum
end;
case r1 > r2 ; ::_thesis: S3[k + 1]
hence  S3[k + 1] by A10; ::_thesis: verum
end;
end;
end;
hence  S3[k + 1] ; ::_thesis: verum
end;
A18: S3[ 0 ] by A9;
A19: for n4 being Element of NAT holds S3[n4] from NAT_1:sch_1(A18, A17);
defpred S4[ Nat] means ( 0 <= $1 implies s3 . 0 >= s3 . $1 );
A20: for n4 being Element of NAT holds s3 . n4 >= s3 . (n4 + 1)
proof
let n4 be Element of NAT ; ::_thesis: s3 . n4 >= s3 . (n4 + 1)
reconsider r2 = s1 . (n4 + 1) as real number ;
 dom s3 = NAT by FUNCT_2:def_1;
then reconsider r1 = s2 . n4 as real number ;
now__::_thesis:_(_(_r1_<=_r2_&_s3_._n4_>=_s3_._(n4_+_1)_)_or_(_r1_>_r2_&_s3_._n4_>=_s3_._(n4_+_1)_)_)
percases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; ::_thesis: s3 . n4 >= s3 . (n4 + 1)
hence  s3 . n4 >= s3 . (n4 + 1) by A10; ::_thesis: verum
end;
case r1 > r2 ; ::_thesis: s3 . n4 >= s3 . (n4 + 1)
hence  s3 . n4 >= s3 . (n4 + 1) by A10; ::_thesis: verum
end;
end;
end;
hence  s3 . n4 >= s3 . (n4 + 1) ; ::_thesis: verum
end;
A21: for k being Element of NAT st S4[k] holds
S4[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] )
assume A22: ( 0 <= k implies s3 . 0 >= s3 . k ) ; ::_thesis: S4[k + 1]
now__::_thesis:_(_0_<=_k_+_1_implies_s3_._0_>=_s3_._(k_+_1)_)
assume  0 <= k + 1 ; ::_thesis: s3 . 0 >= s3 . (k + 1)
A23: s3 . k >= s3 . (k + 1) by A20;
now__::_thesis:_(_(_0_<_k_+_1_&_s3_._0_>=_s3_._(k_+_1)_)_or_(_0_=_k_+_1_&_s3_._0_>=_s3_._(k_+_1)_)_)
percases ( 0 < k + 1 or 0 = k + 1 ) ;
case 0 < k + 1 ; ::_thesis: s3 . 0 >= s3 . (k + 1)
thus  s3 . 0 >= s3 . (k + 1) by A22, A23, XXREAL_0:2; ::_thesis: verum
end;
case 0 = k + 1 ; ::_thesis: s3 . 0 >= s3 . (k + 1)
hence  s3 . 0 >= s3 . (k + 1) ; ::_thesis: verum
end;
end;
end;
hence  s3 . 0 >= s3 . (k + 1) ; ::_thesis: verum
end;
hence  S4[k + 1] ; ::_thesis: verum
end;
defpred S5[ Nat] means  for n4 being Element of NAT st $1 <= n4 holds
s3 . $1 >= s3 . n4;
A24: for k being Element of NAT st S5[k] holds
S5[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S5[k] implies S5[k + 1] )
assume  for n5 being Element of NAT st k <= n5 holds
s3 . k >= s3 . n5 ; ::_thesis: S5[k + 1]
defpred S6[ Nat] means ( k + 1 <= $1 implies s3 . (k + 1) >= s3 . $1 );
A25: for i being Element of NAT st S6[i] holds
S6[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S6[i] implies S6[i + 1] )
reconsider r2 = s1 . (i + 1) as real number ;
 s2 . i in rng s2 by A8, FUNCT_1:def_3;
then reconsider r1 = s2 . i as real number by A11;
A26: now__::_thesis:_(_(_r1_<=_r2_&_s3_._i_>=_s3_._(i_+_1)_)_or_(_r1_>_r2_&_s3_._i_>=_s3_._(i_+_1)_)_)
percases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; ::_thesis: s3 . i >= s3 . (i + 1)
hence  s3 . i >= s3 . (i + 1) by A10; ::_thesis: verum
end;
case r1 > r2 ; ::_thesis: s3 . i >= s3 . (i + 1)
hence  s3 . i >= s3 . (i + 1) by A10; ::_thesis: verum
end;
end;
end;
assume A27: ( k + 1 <= i implies s3 . (k + 1) >= s3 . i ) ; ::_thesis: S6[i + 1]
now__::_thesis:_(_k_+_1_<=_i_+_1_implies_s3_._(k_+_1)_>=_s3_._(i_+_1)_)
assume A28: k + 1 <= i + 1 ; ::_thesis: s3 . (k + 1) >= s3 . (i + 1)
now__::_thesis:_(_(_k_+_1_<_i_+_1_&_s3_._(k_+_1)_>=_s3_._(i_+_1)_)_or_(_k_+_1_=_i_+_1_&_s3_._(k_+_1)_>=_s3_._(i_+_1)_)_)
percases ( k + 1 < i + 1 or k + 1 = i + 1 ) by A28, XXREAL_0:1;
case k + 1 < i + 1 ; ::_thesis: s3 . (k + 1) >= s3 . (i + 1)
hence  s3 . (k + 1) >= s3 . (i + 1) by A27, A26, NAT_1:13, XXREAL_0:2; ::_thesis: verum
end;
case k + 1 = i + 1 ; ::_thesis: s3 . (k + 1) >= s3 . (i + 1)
hence  s3 . (k + 1) >= s3 . (i + 1) ; ::_thesis: verum
end;
end;
end;
hence  s3 . (k + 1) >= s3 . (i + 1) ; ::_thesis: verum
end;
hence  S6[i + 1] ; ::_thesis: verum
end;
A29: S6[ 0 ] ;
thus  for n4 being Element of NAT holds S6[n4] from NAT_1:sch_1(A29, A25); ::_thesis: verum
end;
A30: S4[ 0 ] ;
 for n4 being Element of NAT holds S4[n4] from NAT_1:sch_1(A30, A21);
then A31: S5[ 0 ] ;
 for m4 being Element of NAT holds S5[m4] from NAT_1:sch_1(A31, A24);
then  for m4, n4 being Element of NAT st m4 in dom s3 & n4 in dom s3 & m4 <= n4 holds
s3 . m4 >= s3 . n4 ;
then A32: s3 is non-increasing by SEQM_3:def_4;
A33: rng s3 c= R
proof
defpred S6[ Nat] means s3 . $1 in R;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s3 or y in R )
assume  y in rng s3 ; ::_thesis: y in R
then A34: ex x being set st
( x in dom s3 & y = s3 . x ) by FUNCT_1:def_3;
A35: for k being Element of NAT st S6[k] holds
S6[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S6[k] implies S6[k + 1] )
reconsider r2 = s1 . (k + 1) as real number ;
 s2 . k in rng s2 by A8, FUNCT_1:def_3;
then reconsider r1 = s2 . k as real number by A11;
assume A36: s3 . k in R ; ::_thesis: S6[k + 1]
now__::_thesis:_(_(_r1_<=_r2_&_S6[k_+_1]_)_or_(_r1_>_r2_&_S6[k_+_1]_)_)
percases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; ::_thesis: S6[k + 1]
hence  S6[k + 1] by A10, A36; ::_thesis: verum
end;
case r1 > r2 ; ::_thesis: S6[k + 1]
then  s2 . (k + 1) = s1 . (k + 1) by A10;
hence  S6[k + 1] by A5; ::_thesis: verum
end;
end;
end;
hence  S6[k + 1] ; ::_thesis: verum
end;
A37: S6[ 0 ] by A5, A9;
 for nn being Element of NAT holds S6[nn] from NAT_1:sch_1(A37, A35);
hence  y in R by A34; ::_thesis: verum
end;
 for n being Element of NAT holds s3 . n > (lower_bound R) - 1
proof
let n be Element of NAT ; ::_thesis: s3 . n > (lower_bound R) - 1
 lower_bound R < (lower_bound R) + 1 by XREAL_1:29;
then A38: lower_bound R > (lower_bound R) - 1 by XREAL_1:19;
 s3 . n in rng s3 by A8, FUNCT_1:def_3;
then  s3 . n >= lower_bound R by A1, A33, SEQ_4:def_2;
hence  s3 . n > (lower_bound R) - 1 by A38, XXREAL_0:2; ::_thesis: verum
end;
then A39: s3 is bounded_below by SEQ_2:def_4;
A40: for r being Real st r > 0 holds
(lower_bound R) + r > lim s3
proof
let r be Real; ::_thesis: ( r > 0 implies (lower_bound R) + r > lim s3 )
assume A41: r > 0 ; ::_thesis: (lower_bound R) + r > lim s3
consider n2 being Element of NAT  such that
A42: 1 / r < n2 by SEQ_4:3;
 n2 < n2 + 1 by XREAL_1:29;
then  1 / r < n2 + 1 by A42, XXREAL_0:2;
then  (1 / r) * r < (n2 + 1) * r by A41, XREAL_1:68;
then  1 < (n2 + 1) * r by A41, XCMPLX_1:106;
then  1 / (n2 + 1) < ((n2 + 1) * r) / (n2 + 1) by XREAL_1:74;
then  1 / (n2 + 1) < r by XCMPLX_1:89;
then  rs + (1 / (n2 + 1)) < rs + r by XREAL_1:8;
then A43: rs + r > s1 . n2 by A5, XXREAL_0:2;
A44: s3 . n2 >= lim s3 by A32, A39, SEQ_4:38;
 s1 . n2 >= s3 . n2 by A19;
then  rs + r > s3 . n2 by A43, XXREAL_0:2;
hence  (lower_bound R) + r > lim s3 by A44, XXREAL_0:2; ::_thesis: verum
end;
A45: now__::_thesis:_not_lower_bound_R_<_lim_s3
reconsider r = (lim s3) - (lower_bound R) as Real ;
assume  lower_bound R < lim s3 ; ::_thesis: contradiction
then  r > 0 by XREAL_1:50;
then  (lower_bound R) + ((lim s3) + (- (lower_bound R))) > lim s3 by A40;
hence  contradiction ; ::_thesis: verum
end;
A46: for n being Element of NAT holds s3 . n >= lower_bound R
proof
let n be Element of NAT ; ::_thesis: s3 . n >= lower_bound R
 dom s3 = NAT by FUNCT_2:def_1;
then  s3 . n in rng s3 by FUNCT_1:def_3;
hence  s3 . n >= lower_bound R by A1, A33, SEQ_4:def_2; ::_thesis: verum
end;
 for n being Element of NAT holds s3 . n > (lower_bound R) - 1
proof
let n be Element of NAT ; ::_thesis: s3 . n > (lower_bound R) - 1
 lower_bound R < (lower_bound R) + 1 by XREAL_1:29;
then A47: lower_bound R > (lower_bound R) - 1 by XREAL_1:19;
 s3 . n >= lower_bound R by A46;
hence  s3 . n > (lower_bound R) - 1 by A47, XXREAL_0:2; ::_thesis: verum
end;
then A48: s3 is bounded_below by SEQ_2:def_4;
then  lim s3 >= lower_bound R by A32, A46, PREPOWER:1;
hence  ex s being Real_Sequence st
( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R ) by A32, A33, A48, A45, XXREAL_0:1; ::_thesis: verum
end;

theorem Th13: :: TOPMETR3:13
for X being non empty MetrSpace
for f being Function of I[01],(TopSpaceMetr X)
for F1, F2 being Subset of (TopSpaceMetr X)
for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
proof
let X be non empty MetrSpace; ::_thesis: for f being Function of I[01],(TopSpaceMetr X)
for F1, F2 being Subset of (TopSpaceMetr X)
for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
let f be Function of I[01],(TopSpaceMetr X); ::_thesis: for F1, F2 being Subset of (TopSpaceMetr X)
for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
let F1, F2 be Subset of (TopSpaceMetr X); ::_thesis: for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
let r1, r2 be Real; ::_thesis: ( 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X implies ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) )
assume that
A1: 0 <= r1 and
A2: r2 <= 1 and
A3: ( r1 <= r2 & f . r1 in F1 ) and
A4: f . r2 in F2 and
A5: F1 is closed and
A6: F2 is closed and
A7: f is continuous and
A8: F1 \/ F2 = the carrier of X ; ::_thesis: ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )
A9: r1 in  {  r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 )  }  by A3;
  {  r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 )  }  c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 )  }  or x in REAL )
assume  x in  {  r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 )  }  ; ::_thesis: x in REAL
then  ex r3 being Real st
( r3 = x & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;
hence  x in REAL ; ::_thesis: verum
end;
then reconsider R =  {  r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 )  }  as non empty Subset of REAL by A9;
A10: for r being real number st r in R holds
r <= r2
proof
let r be real number ; ::_thesis: ( r in R implies r <= r2 )
assume  r in R ; ::_thesis: r <= r2
then  ex r3 being Real st
( r3 = r & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;
hence  r <= r2 ; ::_thesis: verum
end;
 r2 is UpperBound of R
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in R or r <= r2 )
assume  r in R ; ::_thesis: r <= r2
then  ex r3 being Real st
( r3 = r & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;
hence  r <= r2 ; ::_thesis: verum
end;
then A11: R is bounded_above by XXREAL_2:def_10;
then consider s1 being Real_Sequence such that
A12: ( s1 is non-decreasing & s1 is convergent ) and
A13: rng s1 c= R and
A14: lim s1 = upper_bound R by Th11;
  {  r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 )  }  c= [.0,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 )  }  or x in [.0,1.] )
assume  x in  {  r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 )  }  ; ::_thesis: x in [.0,1.]
then consider r3 being Real such that
A15: ( r3 = x & r1 <= r3 ) and
A16: r3 <= r2 and
 f . r3 in F1 ;
 r3 <= 1 by A2, A16, XXREAL_0:2;
hence  x in [.0,1.] by A1, A15, XXREAL_1:1; ::_thesis: verum
end;
then reconsider S1 = s1 as sequence of (Closed-Interval-MSpace (0,1)) by A13, Th5, XBOOLE_1:1;
A17: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def_7;
then reconsider S00 = f * S1 as sequence of X by Th2;
A18: S00 is convergent by A7, A12, A17, Th3, Th8;
dom f = the carrier of I[01] by FUNCT_2:def_1
.= the carrier of (Closed-Interval-MSpace (0,1)) by A17, TOPMETR:12 ;
then  f . (lim S1) in rng f by FUNCT_1:3;
then reconsider t1 = f . (lim S1) as Point of X by TOPMETR:12;
reconsider S2 = s1 as sequence of RealSpace by METRIC_1:def_13;
A19: S1 is convergent by A12, Th8;
then  S2 is convergent by Th7;
then  lim S2 = lim S1 by Th7;
then A20: lim s1 = lim S1 by A12, Th4;
A21: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S00 . m),t1) < r
proof
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S00 . m),t1) < r )
assume  r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S00 . m),t1) < r
then consider r7 being Real such that
A22: r7 > 0 and
A23: for w being Point of (Closed-Interval-MSpace (0,1))
for w1 being Point of X st w1 = f . w & dist ((lim S1),w) < r7 holds
dist (t1,w1) < r by A7, A17, UNIFORM1:4;
consider n0 being Element of NAT  such that
A24: for m being Element of NAT st m >= n0 holds
dist ((S1 . m),(lim S1)) < r7 by A19, A22, TBSP_1:def_3;
 for m being Element of NAT st m >= n0 holds
dist ((S00 . m),t1) < r
proof
let m be Element of NAT ; ::_thesis: ( m >= n0 implies dist ((S00 . m),t1) < r )
 dom S00 = NAT by TBSP_1:4;
then A25: S00 . m = f . (S1 . m) by FUNCT_1:12;
assume  m >= n0 ; ::_thesis: dist ((S00 . m),t1) < r
then  dist ((lim S1),(S1 . m)) < r7 by A24;
hence  dist ((S00 . m),t1) < r by A23, A25; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S00 . m),t1) < r ; ::_thesis: verum
end;
A26: r2 >= upper_bound R by A10, SEQ_4:144;
then A27: r2 in  {  r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 )  }  by A4;
  {  r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 )  }  c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 )  }  or x in REAL )
assume  x in  {  r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 )  }  ; ::_thesis: x in REAL
then  ex r3 being Real st
( r3 = x & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;
hence  x in REAL ; ::_thesis: verum
end;
then reconsider R2 =  {  r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 )  }  as non empty Subset of REAL by A27;
A28: for r being real number st r in R2 holds
r >= upper_bound R
proof
let r be real number ; ::_thesis: ( r in R2 implies r >= upper_bound R )
assume  r in R2 ; ::_thesis: r >= upper_bound R
then  ex r3 being Real st
( r3 = r & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;
hence  r >= upper_bound R ; ::_thesis: verum
end;
 upper_bound R is LowerBound of R2
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in R2 or upper_bound R <= r )
assume  r in R2 ; ::_thesis: upper_bound R <= r
then  ex r3 being Real st
( r3 = r & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;
hence  upper_bound R <= r ; ::_thesis: verum
end;
then A29: R2 is bounded_below by XXREAL_2:def_9;
then consider s2 being Real_Sequence such that
A30: ( s2 is non-increasing & s2 is convergent ) and
A31: rng s2 c= R2 and
A32: lim s2 = lower_bound R2 by Th12;
A33: 0 <= upper_bound R by A1, A9, A11, SEQ_4:def_1;
  {  r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 )  }  c= [.0,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 )  }  or x in [.0,1.] )
assume  x in  {  r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 )  }  ; ::_thesis: x in [.0,1.]
then consider r3 being Real such that
A34: ( r3 = x & upper_bound R <= r3 ) and
A35: r3 <= r2 and
 f . r3 in F2 ;
 r3 <= 1 by A2, A35, XXREAL_0:2;
hence  x in [.0,1.] by A33, A34, XXREAL_1:1; ::_thesis: verum
end;
then reconsider S1 = s2 as sequence of (Closed-Interval-MSpace (0,1)) by A31, Th5, XBOOLE_1:1;
reconsider S2 = s2 as sequence of RealSpace by METRIC_1:def_13;
A36: S1 is convergent by A30, Th8;
then  S2 is convergent by Th7;
then  lim S2 = lim S1 by Th7;
then A37: lim s2 = lim S1 by A30, Th4;
 for n4 being Element of NAT holds S00 . n4 in F1
proof
let n4 be Element of NAT ; ::_thesis: S00 . n4 in F1
 dom s1 = NAT by FUNCT_2:def_1;
then  s1 . n4 in rng s1 by FUNCT_1:def_3;
then  s1 . n4 in R by A13;
then  ( dom S00 = NAT & ex r3 being Real st
( r3 = s1 . n4 & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ) by TBSP_1:4;
hence  S00 . n4 in F1 by FUNCT_1:12; ::_thesis: verum
end;
then  lim S00 in F1 by A5, A7, A19, A17, Th1, Th3;
then A38: f . (lim s1) in F1 by A20, A18, A21, TBSP_1:def_3;
A39: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def_7;
then reconsider S00 = f * S1 as sequence of X by Th2;
dom f = the carrier of I[01] by FUNCT_2:def_1
.= the carrier of (Closed-Interval-MSpace (0,1)) by A39, TOPMETR:12 ;
then  f . (lim S1) in rng f by FUNCT_1:3;
then reconsider t1 = f . (lim S1) as Point of X by TOPMETR:12;
A40: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S00 . m),t1) < r
proof
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S00 . m),t1) < r )
assume  r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S00 . m),t1) < r
then consider r7 being Real such that
A41: r7 > 0 and
A42: for w being Point of (Closed-Interval-MSpace (0,1))
for w1 being Point of X st w1 = f . w & dist ((lim S1),w) < r7 holds
dist (t1,w1) < r by A7, A39, UNIFORM1:4;
consider n0 being Element of NAT  such that
A43: for m being Element of NAT st m >= n0 holds
dist ((S1 . m),(lim S1)) < r7 by A36, A41, TBSP_1:def_3;
 for m being Element of NAT st m >= n0 holds
dist ((S00 . m),t1) < r
proof
let m be Element of NAT ; ::_thesis: ( m >= n0 implies dist ((S00 . m),t1) < r )
 dom S00 = NAT by TBSP_1:4;
then A44: S00 . m = f . (S1 . m) by FUNCT_1:12;
assume  m >= n0 ; ::_thesis: dist ((S00 . m),t1) < r
then  dist ((lim S1),(S1 . m)) < r7 by A43;
hence  dist ((S00 . m),t1) < r by A42, A44; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S00 . m),t1) < r ; ::_thesis: verum
end;
A45: r1 <= upper_bound R by A9, A11, SEQ_4:def_1;
 for s being real number st 0 < s holds
ex r being real number st
( r in R2 & r < (upper_bound R) + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in R2 & r < (upper_bound R) + s ) )
assume A46: 0 < s ; ::_thesis: ex r being real number st
( r in R2 & r < (upper_bound R) + s )
now__::_thesis:_ex_r_being_real_number_st_
(_r_<_(upper_bound_R)_+_s_&_r_in_R2_)
assume A47: for r being real number st r < (upper_bound R) + s holds
not r in R2 ; ::_thesis: contradiction
now__::_thesis:_(_(_r2_-_(upper_bound_R)_=_0_&_contradiction_)_or_(_r2_-_(upper_bound_R)_>_0_&_contradiction_)_)
percases ( r2 - (upper_bound R) = 0 or r2 - (upper_bound R) > 0 ) by A26, XREAL_1:48;
case r2 - (upper_bound R) = 0 ; ::_thesis: contradiction
hence  contradiction by A27, A46, A47, XREAL_1:29; ::_thesis: verum
end;
caseA48: r2 - (upper_bound R) > 0 ; ::_thesis: contradiction
set rs0 = min ((r2 - (upper_bound R)),s);
set r0 = (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2);
A49: min ((r2 - (upper_bound R)),s) > 0 by A46, A48, XXREAL_0:21;
then A50: upper_bound R < (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by XREAL_1:29, XREAL_1:215;
 min ((r2 - (upper_bound R)),s) <= r2 - (upper_bound R) by XXREAL_0:17;
then A51: (upper_bound R) + (min ((r2 - (upper_bound R)),s)) <= (upper_bound R) + (r2 - (upper_bound R)) by XREAL_1:7;
A52: (min ((r2 - (upper_bound R)),s)) / 2 < min ((r2 - (upper_bound R)),s) by A49, XREAL_1:216;
then  (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) < (upper_bound R) + (min ((r2 - (upper_bound R)),s)) by XREAL_1:8;
then A53: (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) <= r2 by A51, XXREAL_0:2;
then  (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) <= 1 by A2, XXREAL_0:2;
then  (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in the carrier of I[01] by A1, A45, A49, BORSUK_1:40, XXREAL_1:1;
then  (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in dom f by FUNCT_2:def_1;
then  f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in rng f by FUNCT_1:def_3;
then  f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in the carrier of (TopSpaceMetr X) ;
then  f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in the carrier of X by TOPMETR:12;
then A54: ( f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in F1 or f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in F2 ) by A8, XBOOLE_0:def_3;
 upper_bound R <= (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A49, XREAL_1:29, XREAL_1:215;
then A55: r1 <= (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A45, XXREAL_0:2;
 min ((r2 - (upper_bound R)),s) <= s by XXREAL_0:17;
then  (min ((r2 - (upper_bound R)),s)) / 2 < s by A52, XXREAL_0:2;
then  (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) < (upper_bound R) + s by XREAL_1:8;
then A56: not (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in R2 by A47;
 upper_bound R < (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A49, XREAL_1:29, XREAL_1:215;
then  (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in R by A56, A55, A53, A54;
hence  contradiction by A11, A50, SEQ_4:def_1; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  ex r being real number st
( r in R2 & r < (upper_bound R) + s ) ; ::_thesis: verum
end;
then A57: upper_bound R = lower_bound R2 by A28, A29, SEQ_4:def_2;
 S00 is convergent by A7, A30, A39, Th3, Th8;
then A58: f . (lim S1) = lim S00 by A40, TBSP_1:def_3;
 for n4 being Element of NAT holds S00 . n4 in F2
proof
let n4 be Element of NAT ; ::_thesis: S00 . n4 in F2
 dom s2 = NAT by FUNCT_2:def_1;
then  s2 . n4 in rng s2 by FUNCT_1:def_3;
then  s2 . n4 in R2 by A31;
then  ( dom S00 = NAT & ex r3 being Real st
( r3 = s2 . n4 & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ) by TBSP_1:4;
hence  S00 . n4 in F2 by FUNCT_1:12; ::_thesis: verum
end;
then  lim S00 in F2 by A6, A7, A36, A39, Th1, Th3;
then  f . (lim s1) in F1 /\ F2 by A57, A14, A38, A32, A37, A58, XBOOLE_0:def_4;
hence  ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) by A26, A45, A14; ::_thesis: verum
end;

theorem Th14: :: TOPMETR3:14
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for P, P1 being non empty Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 & P1 is_an_arc_of p2,p1 & P1 c= P holds
P1 = P
proof
let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for P, P1 being non empty Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 & P1 is_an_arc_of p2,p1 & P1 c= P holds
P1 = P
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for P, P1 being non empty Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 & P1 is_an_arc_of p2,p1 & P1 c= P holds
P1 = P
let P, P1 be non empty Subset of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 & P1 is_an_arc_of p2,p1 & P1 c= P implies P1 = P )
assume that
A1: P is_an_arc_of p1,p2 and
A2: P1 is_an_arc_of p2,p1 and
A3: P1 c= P ; ::_thesis: P1 = P
 P1 is_an_arc_of p1,p2 by A2, JORDAN5B:14;
hence  P1 = P by A1, A3, JORDAN6:46; ::_thesis: verum
end;

theorem :: TOPMETR3:15
for P, P1 being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of W-min P, E-max P & P1 c= P & not P1 = Upper_Arc P holds
P1 = Lower_Arc P
proof
let P, P1 be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & P1 is_an_arc_of W-min P, E-max P & P1 c= P & not P1 = Upper_Arc P implies P1 = Lower_Arc P )
assume that
A1: P is being_simple_closed_curve and
A2: P1 is_an_arc_of W-min P, E-max P and
A3: P1 c= P ; ::_thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )
A4: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:def_8;
A5: the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P by PRE_TOPC:def_5 ;
then reconsider U2 = Upper_Arc P as Subset of ((TOP-REAL 2) | P) by A1, JORDAN6:61;
reconsider U3 = Lower_Arc P as Subset of ((TOP-REAL 2) | P) by A1, A5, JORDAN6:61;
A6: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, JORDAN6:def_9;
 U2 = (Upper_Arc P) /\ P by A1, JORDAN6:61, XBOOLE_1:28;
then A7: U2 is closed by A4, JORDAN6:2, JORDAN6:11;
A8: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, JORDAN6:def_9;
 U3 = (Lower_Arc P) /\ P by A1, JORDAN6:61, XBOOLE_1:28;
then A9: U3 is closed by A6, JORDAN6:2, JORDAN6:11;
A10: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A1, JORDAN6:def_9;
then A11: E-max P in (Upper_Arc P) /\ (Lower_Arc P) by TARSKI:def_2;
A12: W-min P in (Upper_Arc P) /\ (Lower_Arc P) by A10, TARSKI:def_2;
consider f being Function of I[01],((TOP-REAL 2) | P1) such that
A13: f is being_homeomorphism and
A14: f . 0 = W-min P and
A15: f . 1 = E-max P by A2, TOPREAL1:def_1;
A16: f is one-to-one by A13, TOPS_2:def_5;
A17: dom f = [#] I[01] by A13, TOPS_2:def_5;
A18: rng f = [#] ((TOP-REAL 2) | P1) by A13, TOPS_2:def_5
.= P1 by PRE_TOPC:def_5 ;
A19: f is continuous by A13, TOPS_2:def_5;
now__::_thesis:_(_(_(_for_r_being_Real_st_0_<_r_&_r_<_1_holds_
f_._r_in_Lower_Arc_P_)_&_(_P1_=_Upper_Arc_P_or_P1_=_Lower_Arc_P_)_)_or_(_ex_r_being_Real_st_
(_0_<_r_&_r_<_1_&_not_f_._r_in_Lower_Arc_P_)_&_(_P1_=_Upper_Arc_P_or_P1_=_Lower_Arc_P_)_)_)
percases ( for r being Real st 0 < r & r < 1 holds
f . r in Lower_Arc P or ex r being Real st
( 0 < r & r < 1 & not f . r in Lower_Arc P ) ) ;
caseA20: for r being Real st 0 < r & r < 1 holds
f . r in Lower_Arc P ; ::_thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )
 P1 c= Lower_Arc P
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P1 or y in Lower_Arc P )
assume  y in P1 ; ::_thesis: y in Lower_Arc P
then consider x being set  such that
A21: x in dom f and
A22: y = f . x by A18, FUNCT_1:def_3;
reconsider r = x as Real by A17, A21, BORSUK_1:40;
A23: r <= 1 by A21, BORSUK_1:40, XXREAL_1:1;
now__::_thesis:_(_(_0_<_r_&_r_<_1_&_y_in_Lower_Arc_P_)_or_(_r_=_0_&_y_in_Lower_Arc_P_)_or_(_r_=_1_&_y_in_Lower_Arc_P_)_)
percases ( ( 0 < r & r < 1 ) or r = 0 or r = 1 ) by A21, A23, BORSUK_1:40, XXREAL_0:1, XXREAL_1:1;
case ( 0 < r & r < 1 ) ; ::_thesis: y in Lower_Arc P
hence  y in Lower_Arc P by A20, A22; ::_thesis: verum
end;
case r = 0 ; ::_thesis: y in Lower_Arc P
hence  y in Lower_Arc P by A12, A14, A22, XBOOLE_0:def_4; ::_thesis: verum
end;
case r = 1 ; ::_thesis: y in Lower_Arc P
hence  y in Lower_Arc P by A11, A15, A22, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence  y in Lower_Arc P ; ::_thesis: verum
end;
hence  ( P1 = Upper_Arc P or P1 = Lower_Arc P ) by A2, A6, Th14; ::_thesis: verum
end;
caseA24: ex r being Real st
( 0 < r & r < 1 & not f . r in Lower_Arc P ) ; ::_thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )
now__::_thesis:_(_(_(_for_r_being_Real_st_0_<_r_&_r_<_1_holds_
f_._r_in_Upper_Arc_P_)_&_(_P1_=_Upper_Arc_P_or_P1_=_Lower_Arc_P_)_)_or_(_ex_r_being_Real_st_
(_0_<_r_&_r_<_1_&_not_f_._r_in_Upper_Arc_P_)_&_contradiction_)_)
percases ( for r being Real st 0 < r & r < 1 holds
f . r in Upper_Arc P or ex r being Real st
( 0 < r & r < 1 & not f . r in Upper_Arc P ) ) ;
caseA25: for r being Real st 0 < r & r < 1 holds
f . r in Upper_Arc P ; ::_thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )
 P1 c= Upper_Arc P
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P1 or y in Upper_Arc P )
assume  y in P1 ; ::_thesis: y in Upper_Arc P
then consider x being set  such that
A26: x in dom f and
A27: y = f . x by A18, FUNCT_1:def_3;
reconsider r = x as Real by A17, A26, BORSUK_1:40;
A28: r <= 1 by A26, BORSUK_1:40, XXREAL_1:1;
now__::_thesis:_(_(_0_<_r_&_r_<_1_&_y_in_Upper_Arc_P_)_or_(_r_=_0_&_y_in_Upper_Arc_P_)_or_(_r_=_1_&_y_in_Upper_Arc_P_)_)
percases ( ( 0 < r & r < 1 ) or r = 0 or r = 1 ) by A26, A28, BORSUK_1:40, XXREAL_0:1, XXREAL_1:1;
case ( 0 < r & r < 1 ) ; ::_thesis: y in Upper_Arc P
hence  y in Upper_Arc P by A25, A27; ::_thesis: verum
end;
case r = 0 ; ::_thesis: y in Upper_Arc P
hence  y in Upper_Arc P by A12, A14, A27, XBOOLE_0:def_4; ::_thesis: verum
end;
case r = 1 ; ::_thesis: y in Upper_Arc P
hence  y in Upper_Arc P by A11, A15, A27, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence  y in Upper_Arc P ; ::_thesis: verum
end;
hence  ( P1 = Upper_Arc P or P1 = Lower_Arc P ) by A2, A4, JORDAN6:46; ::_thesis: verum
end;
case ex r being Real st
( 0 < r & r < 1 & not f . r in Upper_Arc P ) ; ::_thesis: contradiction
then consider r2 being Real such that
A29: 0 < r2 and
A30: r2 < 1 and
A31: not f . r2 in Upper_Arc P ;
 r2 in [.0,1.] by A29, A30, XXREAL_1:1;
then  f . r2 in rng f by A17, BORSUK_1:40, FUNCT_1:def_3;
then A32: f . r2 in Lower_Arc P by A3, A8, A18, A31, XBOOLE_0:def_3;
consider r1 being Real such that
A33: 0 < r1 and
A34: r1 < 1 and
A35: not f . r1 in Lower_Arc P by A24;
 r1 in [.0,1.] by A33, A34, XXREAL_1:1;
then A36: f . r1 in rng f by A17, BORSUK_1:40, FUNCT_1:def_3;
then A37: f . r1 in Upper_Arc P by A3, A8, A18, A35, XBOOLE_0:def_3;
now__::_thesis:_(_(_r1_<=_r2_&_contradiction_)_or_(_r1_>_r2_&_contradiction_)_)
percases ( r1 <= r2 or r1 > r2 ) ;
caseA38: r1 <= r2 ; ::_thesis: contradiction
now__::_thesis:_(_(_r1_=_r2_&_contradiction_)_or_(_r1_<_r2_&_contradiction_)_)
percases ( r1 = r2 or r1 < r2 ) by A38, XXREAL_0:1;
case r1 = r2 ; ::_thesis: contradiction
hence  contradiction by A3, A8, A18, A31, A35, A36, XBOOLE_0:def_3; ::_thesis: verum
end;
caseA39: r1 < r2 ; ::_thesis: contradiction
reconsider Q = P as non empty Subset of (Euclid 2) by TOPREAL3:8;
A40: the carrier of ((TOP-REAL 2) | P1) = [#] ((TOP-REAL 2) | P1)
.= P1 by PRE_TOPC:def_5 ;
the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P by PRE_TOPC:def_5 ;
then  rng f c= the carrier of ((TOP-REAL 2) | P) by A3, A40, XBOOLE_1:1;
then reconsider g = f as Function of I[01],((TOP-REAL 2) | P) by A17, FUNCT_2:2;
 P = P1 \/ P by A3, XBOOLE_1:12;
then A41: (TOP-REAL 2) | P1 is SubSpace of (TOP-REAL 2) | P by TOPMETR:4;
 ( U2 \/ U3 = the carrier of ((Euclid 2) | Q) & (TOP-REAL 2) | P = TopSpaceMetr ((Euclid 2) | Q) ) by A8, EUCLID:63, TOPMETR:def_2;
then consider r0 being Real such that
A42: r1 <= r0 and
A43: r0 <= r2 and
A44: g . r0 in U2 /\ U3 by A19, A7, A9, A30, A33, A32, A37, A39, A41, Th13, PRE_TOPC:26;
 r0 < 1 by A30, A43, XXREAL_0:2;
then A45: r0 in dom f by A17, A33, A42, BORSUK_1:40, XXREAL_1:1;
A46: 1 in dom f by A17, BORSUK_1:40, XXREAL_1:1;
A47: 0 in dom f by A17, BORSUK_1:40, XXREAL_1:1;
now__::_thesis:_(_(_g_._r0_=_W-min_P_&_contradiction_)_or_(_g_._r0_=_E-max_P_&_contradiction_)_)
percases ( g . r0 = W-min P or g . r0 = E-max P ) by A10, A44, TARSKI:def_2;
case g . r0 = W-min P ; ::_thesis: contradiction
hence  contradiction by A14, A16, A33, A42, A45, A47, FUNCT_1:def_4; ::_thesis: verum
end;
case g . r0 = E-max P ; ::_thesis: contradiction
hence  contradiction by A15, A16, A30, A43, A45, A46, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
caseA48: r1 > r2 ; ::_thesis: contradiction
reconsider Q = P as non empty Subset of (Euclid 2) by TOPREAL3:8;
A49: the carrier of ((TOP-REAL 2) | P1) = [#] ((TOP-REAL 2) | P1)
.= P1 by PRE_TOPC:def_5 ;
the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P by PRE_TOPC:def_5 ;
then  rng f c= the carrier of ((TOP-REAL 2) | P) by A3, A49, XBOOLE_1:1;
then reconsider g = f as Function of I[01],((TOP-REAL 2) | P) by A17, FUNCT_2:2;
 P = P1 \/ P by A3, XBOOLE_1:12;
then A50: (TOP-REAL 2) | P1 is SubSpace of (TOP-REAL 2) | P by TOPMETR:4;
 ( U2 \/ U3 = the carrier of ((Euclid 2) | Q) & (TOP-REAL 2) | P = TopSpaceMetr ((Euclid 2) | Q) ) by A8, EUCLID:63, TOPMETR:def_2;
then consider r0 being Real such that
A51: r2 <= r0 and
A52: r0 <= r1 and
A53: g . r0 in U2 /\ U3 by A19, A7, A9, A29, A34, A32, A37, A48, A50, Th13, PRE_TOPC:26;
 r0 < 1 by A34, A52, XXREAL_0:2;
then A54: r0 in dom f by A17, A29, A51, BORSUK_1:40, XXREAL_1:1;
A55: 1 in dom f by A17, BORSUK_1:40, XXREAL_1:1;
A56: 0 in dom f by A17, BORSUK_1:40, XXREAL_1:1;
now__::_thesis:_(_(_g_._r0_=_W-min_P_&_contradiction_)_or_(_g_._r0_=_E-max_P_&_contradiction_)_)
percases ( g . r0 = W-min P or g . r0 = E-max P ) by A10, A53, TARSKI:def_2;
case g . r0 = W-min P ; ::_thesis: contradiction
hence  contradiction by A14, A16, A29, A51, A54, A56, FUNCT_1:def_4; ::_thesis: verum
end;
case g . r0 = E-max P ; ::_thesis: contradiction
hence  contradiction by A15, A16, A34, A52, A54, A55, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  ( P1 = Upper_Arc P or P1 = Lower_Arc P ) ; ::_thesis: verum
end;
end;
end;
hence  ( P1 = Upper_Arc P or P1 = Lower_Arc P ) ; ::_thesis: verum
end;