take f = <*[.r,s.]*>; :: thesis:
A6: rng f = {[.r,s.]} by FINSEQ_1:38;
thus rng f c= F :: thesis:

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng f ; :: thesis:
hence a in F by A5, A6, TARSKI:def 1; :: thesis:

end;

thus union (rng f) = [.r,s.] by A6, ZFMISC_1:25; :: thesis:
thus ( ( for n being natural number st 1 <= n holds
( ( n <= len f implies not f /. n is empty ) & ( n + 1 <= len f implies ( lower_bound (f /. n) <= lower_bound (f /. (n + 1)) & upper_bound (f /. n) <= upper_bound (f /. (n + 1)) & lower_bound (f /. (n + 1)) < upper_bound (f /. n) ) ) & ( n + 2 <= len f implies upper_bound (f /. n) <= lower_bound (f /. (n + 2)) ) ) ) & ( [.r,s.] in F implies f = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being real number st
( r < p & p <= s & f . 1 = [.r,p.[ ) & ex p being real number st
( r <= p & p < s & f . (len f) = ].p,s.] ) & ( for n being natural number st 1 < n & n < len f holds
ex p, q being real number st
( r <= p & p < q & q <= s & f . n = ].p,q.[ ) ) ) ) ) by A4, A5, Lm3; :: thesis:

end;

suppose A7: not [.r,s.] in F ; :: thesis:

set L = Closed-Interval-TSpace (r,s);
A8: the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] by A4, TOPMETR:18;

A9: now

let A be Subset of (Closed-Interval-TSpace (r,s)); :: thesis:
thus ( A is bounded_above & A is bounded_below ) by A8, XXREAL_2:43, XXREAL_2:44; :: thesis:
hence A is bounded Subset of REAL by A8, XBOOLE_1:1; :: thesis:

end;

Closed-Interval-TSpace (r,s) is compact by A4, HEINE:4;
then [#] (Closed-Interval-TSpace (r,s)) is compact by COMPTS_1:1;
then consider G being Subset-Family of (Closed-Interval-TSpace (r,s)) such that
A10: G c= F and
A11: G is Cover of [#] (Closed-Interval-TSpace (r,s)) and
A12: G is finite by A1, A2, COMPTS_1:def 4;
set ZAW = { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ;
set G1 = G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ;
set ALL = { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } ;
set R = RelIncl { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } ;
A13: RelIncl { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } is_antisymmetric_in { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } by WELLORD2:21;
set RM = { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } ;
set LM = { (upper_bound [.r,b.[) where b is Real : [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } ;
A14: G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } c= G by XBOOLE_1:36;
then A15: G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } c= F by A10, XBOOLE_1:1;
A16: for X being set st X in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } holds
X is interval Subset of REAL

proof

let X be set ; :: thesis:
assume X in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ; :: thesis:
then reconsider X = X as connected Subset of (Closed-Interval-TSpace (r,s)) by A3, A15, Def1;
reconsider Y = X as Subset of REAL by A8, XBOOLE_1:1;
Y is interval by Th56;
hence X is interval Subset of REAL ; :: thesis:

end;

reconsider T = Closed-Interval-TSpace (r,s) as non empty connected TopSpace by A4, TREAL_1:20;
set LM1 = { (upper_bound E) where E is Subset of (Closed-Interval-TSpace (r,s)) : E in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } ;
A17: { (upper_bound [.r,b.[) where b is Real : [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } c= { (upper_bound E) where E is Subset of (Closed-Interval-TSpace (r,s)) : E in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (upper_bound [.r,b.[) where b is Real : [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } ; :: thesis:
then ex b being Real st
( x = upper_bound [.r,b.[ & [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) ;
hence x in { (upper_bound E) where E is Subset of (Closed-Interval-TSpace (r,s)) : E in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } ; :: thesis:

end;

A18: { (upper_bound [.r,b.[) where b is Real : [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } c= REAL

proof

end;

set RM1 = { (lower_bound E) where E is Subset of (Closed-Interval-TSpace (r,s)) : E in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } ;
A19: { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } c= { (lower_bound E) where E is Subset of (Closed-Interval-TSpace (r,s)) : E in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } ; :: thesis:
then ex b being Real st
( x = lower_bound ].b,s.] & ].b,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) ;
hence x in { (lower_bound E) where E is Subset of (Closed-Interval-TSpace (r,s)) : E in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } ; :: thesis:

end;

A20: { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } c= REAL

proof

end;

A21: field (RelIncl { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } ) = { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } by WELLORD2:def 1;
( RelIncl { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } is_reflexive_in { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } & RelIncl { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } is_transitive_in { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } ) by WELLORD2:19, WELLORD2:20;
then RelIncl { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } partially_orders { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } by A13, ORDERS_1:def 7;
then consider M being set such that
A22: M is_minimal_in RelIncl { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } by A11, A12, A21, Th61, ORDERS_1:64;
A23: M in field (RelIncl { C where C is Subset-Family of (Closed-Interval-TSpace (r,s)) : ( C is Cover of (Closed-Interval-TSpace (r,s)) & C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) } ) by A22, ORDERS_1:def 12;
then consider C being Subset-Family of (Closed-Interval-TSpace (r,s)) such that
A24: M = C and
A25: C is Cover of (Closed-Interval-TSpace (r,s)) and
A26: C c= G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A21;
A27: union C = [#] (Closed-Interval-TSpace (r,s)) by A25, SETFAM_1:45;
A28: s in [.r,s.] by A4, XXREAL_1:1;
then consider R2 being set such that
A29: s in R2 and
A30: R2 in C by A8, A27, TARSKI:def 4;
r in [.r,s.] by A4, XXREAL_1:1;
then consider R1 being set such that
A31: r in R1 and
A32: R1 in C by A8, A27, TARSKI:def 4;
A33: R1 in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A26, A32;
then A34: R1 in F by A15;
A35: R2 in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A26, A30;
then A36: R2 in F by A15;
reconsider R1 = R1, R2 = R2 as open connected Subset of (Closed-Interval-TSpace (r,s)) by A2, A3, A15, A33, A35, Def1, TOPS_2:def 1;

A37: now

per cases by A4, A7, A29, A36, Th57;

suppose ex a being real number st
( r < a & a <= s & R2 = [.r,a.[ ) ; :: thesis:

hence not { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } is empty by A29, XXREAL_1:3; :: thesis:

end;

suppose ex a being real number st
( r <= a & a < s & R2 = ].a,s.] ) ; :: thesis:

then consider a being real number such that
r <= a and
a < s and
A38: R2 = ].a,s.] ;
a is Real by XREAL_0:def 1;
then lower_bound ].a,s.] in { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } by A26, A30, A38;
hence not { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } is empty ; :: thesis:

end;

suppose ex a, b being real number st
( r <= a & a < b & b <= s & R2 = ].a,b.[ ) ; :: thesis:

end;

A39: now

per cases by A4, A7, A31, A34, Th57;

suppose ex a being real number st
( r < a & a <= s & R1 = [.r,a.[ ) ; :: thesis:

then consider a being real number such that
r < a and
a <= s and
A40: R1 = [.r,a.[ ;
a is Real by XREAL_0:def 1;
then upper_bound [.r,a.[ in { (upper_bound [.r,b.[) where b is Real : [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } by A26, A32, A40;
hence not { (upper_bound [.r,b.[) where b is Real : [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } is empty ; :: thesis:

end;

suppose ex a being real number st
( r <= a & a < s & R1 = ].a,s.] ) ; :: thesis:

hence not { (upper_bound [.r,b.[) where b is Real : [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } is empty by A31, XXREAL_1:2; :: thesis:

end;

suppose ex a, b being real number st
( r <= a & a < b & b <= s & R1 = ].a,b.[ ) ; :: thesis:

end;

A41: G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } is finite by A12;
{ (lower_bound E) where E is Subset of (Closed-Interval-TSpace (r,s)) : E in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } is finite from FRAENKEL:sch 21(A41);
then reconsider RM = { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } as non empty finite Subset of REAL by A19, A37, A20;
F c= bool REAL

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in F ; :: thesis:
then a c= REAL by A8, XBOOLE_1:1;
hence a in bool REAL ; :: thesis:

end;

then G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } c= bool REAL by A15, XBOOLE_1:1;
then reconsider X = C as non empty finite Subset-Family of REAL by A12, A26, A32, XBOOLE_1:1;
{ (upper_bound E) where E is Subset of (Closed-Interval-TSpace (r,s)) : E in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } is finite from FRAENKEL:sch 21(A41);
then reconsider LM = { (upper_bound [.r,b.[) where b is Real : [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } } as non empty finite Subset of REAL by A17, A39, A18;
reconsider kL = max LM as Real by XREAL_0:def 1;
set LEWY = [.r,kL.[;
kL in LM by XXREAL_2:def 8;
then consider b being Real such that
A42: kL = upper_bound [.r,b.[ and
A43: [.r,b.[ in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ;
A44: union G = [#] (Closed-Interval-TSpace (r,s)) by A11, SETFAM_1:45;

A45: now

consider x being set such that
A46: x in the carrier of (Closed-Interval-TSpace (r,s)) by XBOOLE_0:def 1;
consider g being set such that
A47: x in g and
A48: g in G by A44, A46, TARSKI:def 4;
{} c= g by XBOOLE_1:2;
then A49: {} c< g by A47, XBOOLE_0:def 8;
assume A50: {} in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ; :: thesis:
then {} in G by XBOOLE_0:def 5;
then {} in { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A48, A49;
hence contradiction by A50, XBOOLE_0:def 5; :: thesis:

end;

then A51: upper_bound [.r,kL.[ = kL by A42, A43, Th5, XXREAL_1:27;
A52: r < b by A45, A43, XXREAL_1:27;
then r < kL by A42, Th5;
then A53: lower_bound [.r,kL.[ = r by Th4;
reconsider LEWY = [.r,kL.[ as non empty Subset of (Closed-Interval-TSpace (r,s)) by A45, A42, A43, Th5, XXREAL_1:27;
A54: kL = b by A45, A42, A43, Th5, XXREAL_1:27;
A55: for A being Subset of (Closed-Interval-TSpace (r,s)) st r in A & A in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } holds
A = LEWY

proof

let A be Subset of (Closed-Interval-TSpace (r,s)); :: thesis:
assume that
A56: r in A and
A57: A in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ; :: thesis:
A58: ( A in F & A is open ) by A2, A15, A57, TOPS_2:def 1;

A59: now

assume A60: ( ex a being real number st
( r <= a & a < s & A = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & A = ].a,b.[ ) ) ; :: thesis:

per cases by A60;

suppose ex a being real number st
( r <= a & a < s & A = ].a,s.] ) ; :: thesis:

hence contradiction by A56, XXREAL_1:2; :: thesis:

end;

suppose ex a, b being real number st
( r <= a & a < b & b <= s & A = ].a,b.[ ) ; :: thesis:

hence contradiction by A56, XXREAL_1:4; :: thesis:

end;

A is connected by A3, A15, A57, Def1;
then consider ak being real number such that
A61: r < ak and
ak <= s and
A62: A = [.r,ak.[ by A4, A7, A56, A58, A59, Th57;
A63: ak is Real by XREAL_0:def 1;
A64: A c= LEWY

proof

upper_bound A = ak by A61, A62, Th5;
then ak in LM by A57, A62, A63;
then A65: ak <= kL by XXREAL_2:def 8;
let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A66: a in A ; :: thesis:
then a in [.r,s.] by A8;
then reconsider a = a as Real ;
a < ak by A62, A66, XXREAL_1:3;
then A67: a < kL by A65, XXREAL_0:2;
r <= a by A62, A66, XXREAL_1:3;
hence a in LEWY by A67, XXREAL_1:3; :: thesis:

end;

assume A <> LEWY ; :: thesis:
then A c< LEWY by A64, XBOOLE_0:def 8;
then A in { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A14, A43, A54, A57;
hence contradiction by A57, XBOOLE_0:def 5; :: thesis:

end;

then reconsider LLEWY = LEWY as Element of X by A26, A31, A32;
reconsider pP = min RM as Real by XREAL_0:def 1;
set PRAWY = ].pP,s.];
pP in RM by XXREAL_2:def 7;
then consider b being Real such that
A68: pP = lower_bound ].b,s.] and
A69: ].b,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ;
A70: lower_bound ].pP,s.] = pP by A45, A68, A69, Th6, XXREAL_1:26;
A71: b < s by A45, A69, XXREAL_1:26;
then pP < s by A68, Th6;
then A72: upper_bound ].pP,s.] = s by Th7;
reconsider PRAWY = ].pP,s.] as non empty Subset of (Closed-Interval-TSpace (r,s)) by A45, A68, A69, Th6, XXREAL_1:26;
A73: pP = b by A45, A68, A69, Th6, XXREAL_1:26;
A74: for A being Subset of (Closed-Interval-TSpace (r,s)) st A in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } & A <> LEWY & A <> PRAWY holds
ex a, b being Real st
( a < b & A = ].a,b.[ )

proof

let A be Subset of (Closed-Interval-TSpace (r,s)); :: thesis:
assume that
A75: A in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } and
A76: A <> LEWY and
A77: A <> PRAWY ; :: thesis:
A78: ( A in F & A is open & A is connected ) by A2, A3, A15, A75, Def1, TOPS_2:def 1;

per cases by A4, A7, A45, A75, A78, Th57;

suppose ex a being real number st
( r < a & a <= s & A = [.r,a.[ ) ; :: thesis:

then consider a being real number such that
r < a and
a <= s and
A79: A = [.r,a.[ ;

per cases ;

suppose a <= kL ; :: thesis:

then A c= LEWY by A79, XXREAL_1:38;
then A c< LEWY by A76, XBOOLE_0:def 8;
then A in { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A14, A43, A54, A75;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A75, XBOOLE_0:def 5; :: thesis:

end;

suppose a > kL ; :: thesis:

then LEWY c= A by A79, XXREAL_1:38;
then LEWY c< A by A76, XBOOLE_0:def 8;
then LEWY in { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A14, A43, A54, A75;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A43, A54, XBOOLE_0:def 5; :: thesis:

end;

suppose ex a being real number st
( r <= a & a < s & A = ].a,s.] ) ; :: thesis:

then consider a being real number such that
r <= a and
a < s and
A80: A = ].a,s.] ;

per cases ;

suppose a >= pP ; :: thesis:

then A c= PRAWY by A80, XXREAL_1:42;
then A c< PRAWY by A77, XBOOLE_0:def 8;
then A in { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A14, A69, A73, A75;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A75, XBOOLE_0:def 5; :: thesis:

end;

suppose a < pP ; :: thesis:

then PRAWY c= A by A80, XXREAL_1:42;
then PRAWY c< A by A77, XBOOLE_0:def 8;
then PRAWY in { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A14, A69, A73, A75;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A69, A73, XBOOLE_0:def 5; :: thesis:

end;

suppose ex a, b being real number st
( r <= a & a < b & b <= s & A = ].a,b.[ ) ; :: thesis:

then consider a, b being real number such that
r <= a and
A81: a < b and
b <= s and
A82: A = ].a,b.[ ;
reconsider a = a, b = b as Real by XREAL_0:def 1;
take a ; :: thesis:
take b ; :: thesis:
thus ( a < b & A = ].a,b.[ ) by A81, A82; :: thesis:

end;

A83: for A being Subset of (Closed-Interval-TSpace (r,s)) st A in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } & upper_bound A in A holds
A = PRAWY

proof

let A be Subset of (Closed-Interval-TSpace (r,s)); :: thesis:
assume that
A84: A in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } and
A85: upper_bound A in A and
A86: A <> PRAWY ; :: thesis:
A <> LEWY by A51, A85, XXREAL_1:3;
then consider a, b being Real such that
A87: a < b and
A88: A = ].a,b.[ by A74, A84, A86;
upper_bound A = b by A87, A88, TOPREAL6:17;
hence contradiction by A85, A88, XXREAL_1:4; :: thesis:

end;

defpred S₂[ set , set , set ] means ex S being Element of X st
( S = $2 & upper_bound S in $3 );
A89: X c= F by A15, A26, XBOOLE_1:1;
A90: for Z being Subset of REAL st Z in X holds
Z is non empty open connected Subset of T

proof

let Z be Subset of REAL; :: thesis:
assume A91: Z in X ; :: thesis:
then ( not Z is empty & Z is interval ) by A45, A16, A26;
hence Z is non empty open connected Subset of T by A2, A89, A91, Th56, TOPS_2:def 1; :: thesis:

end;

A92: for n being Element of NAT st 1 <= n & n < card X holds
for x being Element of X ex y being Element of X st S₂[n,x,y]

proof

let n be Element of NAT ; :: thesis:
assume that
1 <= n and
n < card X ; :: thesis:
let x be Element of X; :: thesis:
reconsider x1 = x as Subset of REAL ;
A93: not x1 is empty by A90;
A94: x c= union X by ZFMISC_1:74;
then x c= [.r,s.] by A4, A27, TOPMETR:18;
then x1 is bounded_above by XXREAL_2:43;
then upper_bound x is Element of (Closed-Interval-TSpace (r,s)) by A8, A27, A93, A94, Th2;
then consider y being set such that
A95: upper_bound x in y and
A96: y in X by A27, TARSKI:def 4;
reconsider y = y as Element of X by A96;
take y ; :: thesis:
take x ; :: thesis:
thus ( x = x & upper_bound x in y ) by A95; :: thesis:

end;

consider IT being FinSequence of X such that
A97: len IT = card X and
A98: ( IT . 1 = LLEWY or card X = 0 ) and
A99: for n being Element of NAT st 1 <= n & n < card X holds
S₂[n,IT . n,IT . (n + 1)] from RECDEF_1:sch 4(A92);
A100: rng IT c= X ;
rng IT c= bool REAL by XBOOLE_1:1;
then reconsider IT = IT as FinSequence of bool REAL by FINSEQ_1:def 4;
A101: not IT is empty by A97;
then A102: not rng IT is empty ;
then A103: 1 in dom IT by FINSEQ_3:32;
then A104: IT /. 1 = IT . 1 by PARTFUN1:def 6;
A105: for n being natural number st n in dom IT holds
( IT . n in X & IT /. n in X )

proof

let n be natural number ; :: thesis:
assume n in dom IT ; :: thesis:
then ( IT . n = IT /. n & IT . n in rng IT ) by FUNCT_1:def 3, PARTFUN1:def 6;
hence ( IT . n in X & IT /. n in X ) by A100; :: thesis:

end;

A106: for n being natural number st n in dom IT holds
( IT . n in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } & IT /. n in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } )

proof

let n be natural number ; :: thesis:
assume n in dom IT ; :: thesis:
then ( IT . n = IT /. n & IT . n in X ) by A105, PARTFUN1:def 6;
hence ( IT . n in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } & IT /. n in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) by A26; :: thesis:

end;

A107: for i being natural number st i in dom IT holds
for x being Point of (Closed-Interval-TSpace (r,s)) st x < upper_bound (IT /. i) holds
ex j being natural number st
( j in dom IT & j <= i & x in IT /. j )

proof

defpred S₃[ natural number ] means ( $1 in dom IT implies for x being Point of (Closed-Interval-TSpace (r,s)) st x < upper_bound (IT /. $1) holds
ex j being natural number st
( j in dom IT & j <= $1 & x in IT /. j ) );
A108: for n being natural number st S₃[n] holds
S₃[n + 1]

proof

let n be natural number ; :: thesis:
assume that
A109: S₃[n] and
A110: n + 1 in dom IT ; :: thesis:
A111: IT /. (n + 1) = IT . (n + 1) by A110, PARTFUN1:def 6;
let x be Point of (Closed-Interval-TSpace (r,s)); :: thesis:
assume A112: x < upper_bound (IT /. (n + 1)) ; :: thesis:

per cases by A110, TOPREALA:2;

suppose A113: n = 0 ; :: thesis:

take 1 ; :: thesis:
thus 1 in dom IT by A102, FINSEQ_3:32; :: thesis:
thus 1 <= n + 1 by A113; :: thesis:
r <= x by A8, XXREAL_1:1;
hence x in IT /. 1 by A51, A98, A112, A111, A113, XXREAL_1:3; :: thesis:

end;

suppose A114: n in dom IT ; :: thesis:

n + 1 <= len IT by A110, FINSEQ_3:25;
then A115: n < len IT by NAT_1:13;
1 <= n by A114, FINSEQ_3:25;
then A116: ex S being Element of X st
( S = IT . n & upper_bound S in IT . (n + 1) ) by A97, A99, A114, A115;
IT /. (n + 1) in X by A105, A110;
then A117: IT /. (n + 1) is bounded_below by A9;
IT /. n = IT . n by A114, PARTFUN1:def 6;
then A118: lower_bound (IT /. (n + 1)) <= upper_bound (IT /. n) by A111, A117, A116, SEQ_4:def 2;
A119: ( IT /. (n + 1) is interval Subset of REAL & not IT /. (n + 1) is empty ) by A45, A16, A106, A110;

per cases by XXREAL_0:1;

suppose x < upper_bound (IT /. n) ; :: thesis:

then consider j being natural number such that
A120: j in dom IT and
A121: j <= n and
A122: x in IT /. j by A109, A114;
take j ; :: thesis:
thus j in dom IT by A120; :: thesis:
j + 0 < n + 1 by A121, XREAL_1:8;
hence j <= n + 1 ; :: thesis:
thus x in IT /. j by A122; :: thesis:

end;

suppose A123: x = upper_bound (IT /. n) ; :: thesis:

take n + 1 ; :: thesis:
thus n + 1 in dom IT by A110; :: thesis:
thus n + 1 <= n + 1 ; :: thesis:
thus x in IT /. (n + 1) by A111, A114, A116, A123, PARTFUN1:def 6; :: thesis:

end;

suppose A124: x > upper_bound (IT /. n) ; :: thesis:

take n + 1 ; :: thesis:
thus n + 1 in dom IT by A110; :: thesis:
thus n + 1 <= n + 1 ; :: thesis:
lower_bound (IT /. (n + 1)) < x by A118, A124, XXREAL_0:2;
hence x in IT /. (n + 1) by A112, A119, Th42; :: thesis:

end;

A125: S₃[ 0 ] by FINSEQ_3:24;
A126: for n being natural number holds S₃[n] from NAT_1:sch 2(A125, A108);
let i be natural number ; :: thesis:
assume i in dom IT ; :: thesis:
hence for x being Point of (Closed-Interval-TSpace (r,s)) st x < upper_bound (IT /. i) holds
ex j being natural number st
( j in dom IT & j <= i & x in IT /. j ) by A126; :: thesis:

end;

A127: s in ].b,s.] by A71, XXREAL_1:2;
A128: for i being natural number st i in dom IT holds
for j being natural number st j in dom IT & i < j holds
ex y being Point of (Closed-Interval-TSpace (r,s)) st
( y in IT /. j & ( for x being Point of (Closed-Interval-TSpace (r,s)) st x in IT /. i holds
x < y ) )

proof

let i be natural number ; :: thesis:
assume A129: i in dom IT ; :: thesis:
defpred S₃[ natural number ] means ( $1 in dom IT & i < $1 implies ex y being Point of (Closed-Interval-TSpace (r,s)) st
( y in IT /. $1 & ( for x being Point of (Closed-Interval-TSpace (r,s)) st x in IT /. i holds
x < y ) ) );
A130: for n being natural number st S₃[n] holds
S₃[n + 1]

proof

let n be natural number ; :: thesis:
assume that
A131: S₃[n] and
A132: n + 1 in dom IT ; :: thesis:
A133: IT /. (n + 1) = IT . (n + 1) by A132, PARTFUN1:def 6;
assume A134: i < n + 1 ; :: thesis:
then A135: i <= n by NAT_1:13;

per cases by A132, TOPREALA:2;

suppose n = 0 ; :: thesis:

then i = 0 by A134, NAT_1:13;
hence ex y being Point of (Closed-Interval-TSpace (r,s)) st
( y in IT /. (n + 1) & ( for x being Point of (Closed-Interval-TSpace (r,s)) st x in IT /. i holds
x < y ) ) by A129, FINSEQ_3:24; :: thesis:

end;

suppose A136: n in dom IT ; :: thesis:

then A137: IT /. n in X by A105;
then A138: IT /. n is bounded_above by A9;
A139: IT /. n = IT . n by A136, PARTFUN1:def 6;
then IT /. n in rng IT by A136, FUNCT_1:def 3;
then A140: ( not IT /. n is empty & IT /. n is Subset of (Closed-Interval-TSpace (r,s)) ) by A90, A100;
then upper_bound (IT /. n) in [.r,s.] by A8, A138, Th2;
then A141: upper_bound (IT /. n) <= s by XXREAL_1:1;
A142: IT /. (n + 1) in X by A105, A132;
A143: 1 <= n by A136, FINSEQ_3:25;
A144: IT /. (n + 1) in rng IT by A132, A133, FUNCT_1:def 3;
then A145: IT /. (n + 1) is open connected Subset of (Closed-Interval-TSpace (r,s)) by A90, A100;
then A146: IT /. (n + 1) is interval Subset of REAL by Th56;
A147: n + 1 <= len IT by A132, FINSEQ_3:25;
then ( n is Element of NAT & n < card X ) by A97, NAT_1:13, ORDINAL1:def 12;
then consider S being Element of X such that
A148: S = IT . n and
A149: upper_bound S in IT . (n + 1) by A99, A143;
IT /. (n + 1) is bounded_below by A9, A145;
then A150: lower_bound (IT /. (n + 1)) <= upper_bound S by A133, A149, SEQ_4:def 2;
A151: IT /. (n + 1) is bounded_above by A9, A145;
then A152: upper_bound S <= upper_bound (IT /. (n + 1)) by A133, A149, SEQ_4:def 1;
A153: not IT /. (n + 1) is empty by A90, A100, A144;
then upper_bound (IT /. (n + 1)) in [.r,s.] by A8, A145, A151, Th2;
then A154: upper_bound (IT /. (n + 1)) <= s by XXREAL_1:1;

per cases by A135, XXREAL_0:1;

suppose i < n ; :: thesis:

then consider y being Point of (Closed-Interval-TSpace (r,s)) such that
A155: y in IT /. n and
A156: for x being Point of (Closed-Interval-TSpace (r,s)) st x in IT /. i holds
x < y by A131, A136;
A157: y <= upper_bound (IT /. n) by A138, A155, SEQ_4:def 1;

per cases by A152, XXREAL_0:1;

suppose A158: upper_bound S < upper_bound (IT /. (n + 1)) ; :: thesis:

end;

suppose A161: upper_bound S = upper_bound (IT /. (n + 1)) ; :: thesis:

reconsider y1 = s as Point of (Closed-Interval-TSpace (r,s)) by A4, A8, XXREAL_1:1;
take y1 ; :: thesis:
IT /. (n + 1) = PRAWY by A26, A83, A133, A149, A142, A161;
hence y1 in IT /. (n + 1) by A71, A73, XXREAL_1:2; :: thesis:
let x be Point of (Closed-Interval-TSpace (r,s)); :: thesis:
assume x in IT /. i ; :: thesis:
then x < upper_bound (IT /. n) by A156, A157, XXREAL_0:2;
hence x < y1 by A141, XXREAL_0:2; :: thesis:

end;

suppose A162: i = n ; :: thesis:

reconsider y1 = upper_bound (IT /. n) as Element of (Closed-Interval-TSpace (r,s)) by A8, A138, A140, Th2;
take y1 ; :: thesis:
thus y1 in IT /. (n + 1) by A133, A136, A148, A149, PARTFUN1:def 6; :: thesis:
let x be Point of (Closed-Interval-TSpace (r,s)); :: thesis:
assume A163: x in IT /. i ; :: thesis:

A164: now

set IT1 = IT | (Seg n);
A165: rng (IT | (Seg n)) c= rng IT by RELAT_1:70;
rng (IT | (Seg n)) c= bool the carrier of (Closed-Interval-TSpace (r,s))

proof

let A be set ; :: according to TARSKI:def 3 :: thesis:
assume A in rng (IT | (Seg n)) ; :: thesis:
then A in rng IT by A165;
then A in X by A100;
hence A in bool the carrier of (Closed-Interval-TSpace (r,s)) ; :: thesis:

end;

then reconsider FI = rng (IT | (Seg n)) as Subset-Family of (Closed-Interval-TSpace (r,s)) ;
assume x = upper_bound (IT /. n) ; :: thesis:
then A166: IT /. n = PRAWY by A26, A83, A137, A162, A163;

A167: now

union FI = the carrier of (Closed-Interval-TSpace (r,s))

proof

thus union FI c= the carrier of (Closed-Interval-TSpace (r,s)) ; :: according to XBOOLE_0:def 10 :: thesis:
let l be set ; :: according to TARSKI:def 3 :: thesis:
assume l in the carrier of (Closed-Interval-TSpace (r,s)) ; :: thesis:
then reconsider l = l as Point of (Closed-Interval-TSpace (r,s)) ;

per cases ;

suppose l < upper_bound (IT /. n) ; :: thesis:

then consider j being natural number such that
A168: j in dom IT and
A169: j <= n and
A170: l in IT /. j by A107, A136;
1 <= j by A168, FINSEQ_3:25;
then j in Seg n by A169, FINSEQ_1:1;
then A171: IT . j in FI by A168, FUNCT_1:50;
IT . j = IT /. j by A168, PARTFUN1:def 6;
hence l in union FI by A170, A171, TARSKI:def 4; :: thesis:

end;

suppose A172: l >= upper_bound (IT /. n) ; :: thesis:

n in Seg n by A143, FINSEQ_1:1;
then A173: IT . n in FI by A136, FUNCT_1:50;
l <= s by A8, XXREAL_1:1;
then l = s by A72, A166, A172, XXREAL_0:1;
hence l in union FI by A73, A127, A139, A166, A173, TARSKI:def 4; :: thesis:

end;

end;

Seg n c= dom IT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
A178: n + 0 <= n + 1 by XREAL_1:6;
assume A179: x in Seg n ; :: thesis:
then reconsider x = x as Nat ;
x <= n by A179, FINSEQ_1:1;
then x <= n + 1 by A178, XXREAL_0:2;
then A180: x <= len IT by A147, XXREAL_0:2;
1 <= x by A179, FINSEQ_1:1;
hence x in dom IT by A180, FINSEQ_3:25; :: thesis:

end;

then dom (IT | (Seg n)) = Seg n by RELAT_1:62;
then ( card (rng (IT | (Seg n))) <= card (dom (IT | (Seg n))) & card (dom (IT | (Seg n))) = n ) by CARD_2:47, FINSEQ_1:57;
then n + 1 <= n + 0 by A97, A147, A167, XXREAL_0:2;
hence contradiction by XREAL_1:6; :: thesis:

end;

x <= upper_bound (IT /. n) by A138, A162, A163, SEQ_4:def 1;
hence x < y1 by A164, XXREAL_0:1; :: thesis:

end;

A181: S₃[ 0 ] ;
for n being natural number holds S₃[n] from NAT_1:sch 2(A181, A130);
hence for j being natural number st j in dom IT & i < j holds
ex y being Point of (Closed-Interval-TSpace (r,s)) st
( y in IT /. j & ( for x being Point of (Closed-Interval-TSpace (r,s)) st x in IT /. i holds
x < y ) ) ; :: thesis:

end;

A182: IT is one-to-one

proof

let i, j be set ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A183: ( i in dom IT & j in dom IT ) and
A184: IT . i = IT . j ; :: thesis:
A185: ( IT /. i = IT . i & IT /. j = IT . j ) by A183, PARTFUN1:def 6;
assume A186: i <> j ; :: thesis:
reconsider i = i, j = j as Nat by A183;

per cases by A186, XXREAL_0:1;

suppose i < j ; :: thesis:

then ex y being Point of (Closed-Interval-TSpace (r,s)) st
( y in IT /. j & ( for x being Point of (Closed-Interval-TSpace (r,s)) st x in IT /. i holds
x < y ) ) by A128, A183;
hence contradiction by A184, A185; :: thesis:

end;

suppose j < i ; :: thesis:

then ex y being Point of (Closed-Interval-TSpace (r,s)) st
( y in IT /. i & ( for x being Point of (Closed-Interval-TSpace (r,s)) st x in IT /. j holds
x < y ) ) by A128, A183;
hence contradiction by A184, A185; :: thesis:

end;

A187: for i, j being natural number st i in dom IT & j in dom IT & i <> j holds
IT /. i <> IT /. j

proof

let i, j be natural number ; :: thesis:
assume that
A188: ( i in dom IT & j in dom IT ) and
A189: i <> j ; :: thesis:
( IT /. i = IT . i & IT /. j = IT . j ) by A188, PARTFUN1:def 6;
hence IT /. i <> IT /. j by A182, A188, A189, FUNCT_1:def 4; :: thesis:

end;

A190: for A being Subset of (Closed-Interval-TSpace (r,s)) st s in A & A in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } holds
A = PRAWY

proof

let A be Subset of (Closed-Interval-TSpace (r,s)); :: thesis:
assume that
A191: s in A and
A192: A in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ; :: thesis:
A193: ( A in F & A is open ) by A2, A15, A192, TOPS_2:def 1;

A194: now

assume A195: ( ex a being real number st
( r < a & a <= s & A = [.r,a.[ ) or ex a, b being real number st
( r <= a & a < b & b <= s & A = ].a,b.[ ) ) ; :: thesis:

per cases by A195;

suppose ex a being real number st
( r < a & a <= s & A = [.r,a.[ ) ; :: thesis:

hence contradiction by A191, XXREAL_1:3; :: thesis:

end;

suppose ex a, b being real number st
( r <= a & a < b & b <= s & A = ].a,b.[ ) ; :: thesis:

hence contradiction by A191, XXREAL_1:4; :: thesis:

end;

A is connected by A3, A15, A192, Def1;
then consider ak being real number such that
r <= ak and
A196: ak < s and
A197: A = ].ak,s.] by A4, A7, A191, A193, A194, Th57;
A198: ak is Real by XREAL_0:def 1;
A199: A c= PRAWY

proof

lower_bound A = ak by A196, A197, Th6;
then ak in RM by A192, A197, A198;
then A200: pP <= ak by XXREAL_2:def 7;
let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A201: a in A ; :: thesis:
then a in [.r,s.] by A8;
then reconsider a = a as Real ;
ak < a by A197, A201, XXREAL_1:2;
then A202: pP < a by A200, XXREAL_0:2;
a <= s by A197, A201, XXREAL_1:2;
hence a in PRAWY by A202, XXREAL_1:2; :: thesis:

end;

assume A <> PRAWY ; :: thesis:
then A c< PRAWY by A199, XBOOLE_0:def 8;
then A in { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A14, A69, A73, A192;
hence contradiction by A192, XBOOLE_0:def 5; :: thesis:

end;

take IT ; :: thesis:
thus rng IT c= F by A89, A100, XBOOLE_1:1; :: thesis:
dom IT = Seg (len IT) by FINSEQ_1:def 3;
then A203: card (dom IT) = card X by A97, FINSEQ_1:57;
IT is Function of (dom IT),X by A100, FUNCT_2:2;
then A204: rng IT = X by A203, A182, FINSEQ_4:63;
hence union (rng IT) = [.r,s.] by A4, A27, TOPMETR:18; :: thesis:
ex Z being set st
( s in Z & Z in C ) by A28, A8, A27, TARSKI:def 4;
then PRAWY in X by A26, A190;
then consider i being set such that
A205: i in dom IT and
A206: IT . i = PRAWY by A204, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A205;
A207: i <= len IT by A205, FINSEQ_3:25;
A208: IT /. i = IT . i by A205, PARTFUN1:def 6;
A209: 1 <= i by A205, FINSEQ_3:25;

A210: now

assume i <> len IT ; :: thesis:
then A211: i < len IT by A207, XXREAL_0:1;
then A212: ex S being Element of X st
( S = IT . i & upper_bound S in IT . (i + 1) ) by A97, A99, A209;
( 0 + 1 <= i + 1 & i + 1 <= len IT ) by A211, NAT_1:13;
then A213: i + 1 in dom IT by FINSEQ_3:25;
then ( IT /. (i + 1) = IT . (i + 1) & IT /. (i + 1) in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } ) by A106, PARTFUN1:def 6;
then i + 0 = i + 1 by A72, A190, A187, A205, A206, A208, A212, A213;
hence contradiction ; :: thesis:

end;

A214: len IT in dom IT by A101, FINSEQ_5:6;
A215: for n being natural number st 1 < n & n < len IT holds
ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ )

proof

let n be natural number ; :: thesis:
assume that
A216: 1 < n and
A217: n < len IT ; :: thesis:
A218: n in dom IT by A216, A217, FINSEQ_3:25;
then IT . n in rng IT by FUNCT_1:def 3;
then A219: IT /. n in rng IT by A218, PARTFUN1:def 6;
then A220: IT /. n in X by A100;
then A221: ( IT /. n in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } & IT /. n in F ) by A26, A89;
A222: IT /. n is open connected Subset of (Closed-Interval-TSpace (r,s)) by A90, A100, A219;

per cases by A4, A7, A45, A221, A222, Th57;

suppose ex a being real number st
( r < a & a <= s & IT /. n = [.r,a.[ ) ; :: thesis:

then consider a being real number such that
A223: r < a and
a <= s and
A224: IT /. n = [.r,a.[ ;
r in [.r,a.[ by A223, XXREAL_1:3;
hence ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A26, A55, A98, A103, A104, A187, A216, A218, A220, A224; :: thesis:

end;

suppose ex a being real number st
( r <= a & a < s & IT /. n = ].a,s.] ) ; :: thesis:

then consider a being real number such that
r <= a and
A225: a < s and
A226: IT /. n = ].a,s.] ;
( upper_bound ].a,s.] = s & s in ].a,s.] ) by A225, Th7, XXREAL_1:2;
hence ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A26, A83, A214, A187, A206, A208, A210, A217, A218, A220, A226; :: thesis:

end;

suppose ex a, b being real number st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) ; :: thesis:

then consider a, b being real number such that
A227: ( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) ;
reconsider a = a, b = b as Real by XREAL_0:def 1;
take a ; :: thesis:
take b ; :: thesis:
thus ( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A227; :: thesis:

end;

A228: now

let n be natural number ; :: thesis:
assume A229: 1 <= n ; :: thesis:
reconsider m = n as Element of NAT by ORDINAL1:def 12;

hereby :: thesis:

assume n <= len IT ; :: thesis:
then ( m in dom IT & IT /. n = IT . n ) by A229, FINSEQ_3:25, FINSEQ_4:15;
then IT /. n in rng IT by FUNCT_1:def 3;
then IT /. n in X by A100;
hence not IT /. n is empty by A45, A26; :: thesis:

end;

hereby :: thesis:

assume A230: n + 1 <= len IT ; :: thesis:
then A231: m < len IT by NAT_1:13;
then A232: IT /. n = IT . n by A229, FINSEQ_4:15;
A233: m in dom IT by A229, A231, FINSEQ_3:25;
then IT /. n in rng IT by A232, FUNCT_1:def 3;
then A234: IT /. n in X by A100;
then A235: IT /. n in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A26;
A236: IT /. n is non empty bounded interval Subset of REAL by A9, A45, A16, A26, A234;
A237: ex S being Element of X st
( S = IT . n & upper_bound S in IT . (n + 1) ) by A97, A99, A229, A231;
A238: 1 < m + 1 by A229, NAT_1:13;
then A239: IT /. (m + 1) = IT . (m + 1) by A230, FINSEQ_4:15;
A240: n + 1 in dom IT by A230, A238, FINSEQ_3:25;
then A241: IT /. (n + 1) in rng IT by A239, FUNCT_1:def 3;
then A242: IT /. (n + 1) in X by A100;
then A243: IT /. (n + 1) in G \ { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A26;
n + 0 < n + 1 by XREAL_1:6;
then A244: IT /. n <> IT /. (n + 1) by A187, A233, A240;
A245: IT /. (n + 1) is non empty bounded interval Subset of REAL by A9, A45, A16, A26, A242;
IT /. (n + 1) c= union X by A100, A241, ZFMISC_1:74;
then IT /. (n + 1) c= [.r,s.] by A4, A27, TOPMETR:18;
then A246: IT /. (n + 1) is bounded_above by XXREAL_2:43;
then A247: upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) by A237, A232, A239, SEQ_4:def 1;

hereby :: thesis:

assume A248: lower_bound (IT /. n) > lower_bound (IT /. (n + 1)) ; :: thesis:
( upper_bound (IT /. (n + 1)) = upper_bound (IT /. n) & upper_bound (IT /. n) in IT /. n implies upper_bound (IT /. (n + 1)) in IT /. (n + 1) ) by A26, A83, A214, A187, A206, A208, A210, A231, A233, A234;
then IT /. n c= IT /. (n + 1) by A236, A245, A247, A248, Th43;
then IT /. n c< IT /. (n + 1) by A244, XBOOLE_0:def 8;
then IT /. n in { X where X is Subset of (Closed-Interval-TSpace (r,s)) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace (r,s)) st
( Y in G & X c< Y ) ) } by A14, A235, A243;
hence contradiction by A26, A234, XBOOLE_0:def 5; :: thesis:

end;

thus upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) by A237, A232, A239, A246, SEQ_4:def 1; :: thesis:

per cases by A230, XXREAL_0:1;

suppose A249: n + 1 = len IT ; :: thesis:

then pP < upper_bound (IT /. n) by A206, A210, A237, A232, XXREAL_1:2;
hence lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) by A206, A208, A210, A249, Th6, XXREAL_1:26; :: thesis:

end;

suppose n + 1 < len IT ; :: thesis:

then consider a1, b1 being Real such that
r <= a1 and
A250: a1 < b1 and
b1 <= s and
A251: IT /. (n + 1) = ].a1,b1.[ by A215, A238;
a1 < upper_bound (IT /. n) by A237, A232, A239, A251, XXREAL_1:4;
hence lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) by A250, A251, TOPREAL6:17; :: thesis:

end;

hereby :: thesis:

let n be natural number ; :: thesis:
assume A252: 1 <= n ; :: thesis:
thus A253: ( ( n <= len IT implies not IT /. n is empty ) & ( n + 1 <= len IT implies ( lower_bound (IT /. n) <= lower_bound (IT /. (n + 1)) & upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) & lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) ) ) ) by A228, A252; :: thesis:
reconsider m = n as Nat ;
A254: n + 0 < n + 1 by XREAL_1:6;
then A255: 1 < m + 1 by A252, XXREAL_0:2;
assume A256: n + 2 <= len IT ; :: thesis:
then A257: (n + 1) + 1 <= len IT ;
then A258: m + 1 < len IT by NAT_1:13;
then A259: n + 1 in dom IT by A255, FINSEQ_3:25;
then IT /. (n + 1) = IT . (n + 1) by PARTFUN1:def 6;
then IT /. (n + 1) in rng IT by A259, FUNCT_1:def 3;
then A260: IT /. (n + 1) in X by A100;
0 + 1 <= n + 1 by XREAL_1:6;
then A261: upper_bound (IT /. (n + 1)) <= upper_bound (IT /. ((n + 1) + 1)) by A228, A256;
assume A262: upper_bound (IT /. n) > lower_bound (IT /. (n + 2)) ; :: thesis:
consider a1, b1 being Real such that
r <= a1 and
A263: a1 < b1 and
b1 <= s and
A264: IT /. (n + 1) = ].a1,b1.[ by A215, A255, A258;
A265: lower_bound ].a1,b1.[ = a1 by A263, TOPREAL6:17;
A266: upper_bound ].a1,b1.[ = b1 by A263, TOPREAL6:17;
A267: IT /. (n + 1) c= (IT /. n) \/ (IT /. (n + 2))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A268: x in IT /. (n + 1) ; :: thesis:
then reconsider x = x as Real ;
A269: a1 < x by A264, A268, XXREAL_1:4;
A270: x < b1 by A264, A268, XXREAL_1:4;

per cases ;

suppose A271: x < upper_bound (IT /. n) ; :: thesis:

per cases ;

suppose A272: n = 1 ; :: thesis:

then lower_bound (IT /. n) <= x by A8, A53, A98, A104, A260, A268, XXREAL_1:1;
then x in IT /. n by A42, A54, A53, A98, A104, A271, A272, XXREAL_1:3;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

suppose A273: n <> 1 ; :: thesis:

n + 0 < n + 2 by XREAL_1:6;
then A274: n < len IT by A256, XXREAL_0:2;
A275: lower_bound (IT /. n) < x by A253, A257, A264, A265, A269, NAT_1:13, XXREAL_0:2;
1 < n by A252, A273, XXREAL_0:1;
then consider a, b being Real such that
r <= a and
A276: a < b and
b <= s and
A277: IT /. n = ].a,b.[ by A215, A274;
( lower_bound (IT /. n) = a & upper_bound (IT /. n) = b ) by A276, A277, TOPREAL6:17;
then x in IT /. n by A271, A277, A275, XXREAL_1:4;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

suppose x >= upper_bound (IT /. n) ; :: thesis:

then A278: x > lower_bound (IT /. (n + 2)) by A262, XXREAL_0:2;

per cases ;

suppose A279: len IT = n + 2 ; :: thesis:

x <= s by A8, A260, A268, XXREAL_1:1;
then x in IT /. (n + 2) by A70, A206, A208, A210, A278, A279, XXREAL_1:2;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

suppose A280: len IT <> n + 2 ; :: thesis:

n + 1 < n + 2 by XREAL_1:6;
then A281: 1 < n + 2 by A255, XXREAL_0:2;
(n + 1) + 1 < len IT by A256, A280, XXREAL_0:1;
then consider a2, b2 being Real such that
r <= a2 and
A282: a2 < b2 and
b2 <= s and
A283: IT /. (n + 2) = ].a2,b2.[ by A215, A281;
upper_bound ].a2,b2.[ = b2 by A282, TOPREAL6:17;
then A284: x < b2 by A261, A264, A266, A270, A283, XXREAL_0:2;
lower_bound ].a2,b2.[ = a2 by A282, TOPREAL6:17;
then x in IT /. (n + 2) by A278, A283, A284, XXREAL_1:4;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

m + 1 <= m + 2 by XREAL_1:6;
then 1 <= m + 2 by A255, XXREAL_0:2;
then A285: m + 2 in dom IT by A256, FINSEQ_3:25;
then IT /. (n + 2) = IT . (n + 2) by PARTFUN1:def 6;
then IT /. (n + 2) in rng IT by A285, FUNCT_1:def 3;
then A286: IT /. (n + 2) in X by A100;
m <= len IT by A254, A258, XXREAL_0:2;
then A287: n in dom IT by A252, FINSEQ_3:25;
then IT /. n = IT . n by PARTFUN1:def 6;
then IT /. n in rng IT by A287, FUNCT_1:def 3;
then A288: IT /. n in X by A100;
n + 1 < n + 2 by XREAL_1:6;
then A289: IT /. (n + 2) <> IT /. (n + 1) by A187, A259, A285;
n + 0 < n + 1 by XREAL_1:6;
then IT /. n <> IT /. (n + 1) by A187, A287, A259;
hence contradiction by A22, A23, A24, A288, A260, A286, A289, A267, Th62; :: thesis:

end;

thus ( [.r,s.] in F implies IT = <*[.r,s.]*> ) by A7; :: thesis:
assume not [.r,s.] in F ; :: thesis:
thus ex p being real number st
( r < p & p <= s & IT . 1 = [.r,p.[ ) :: thesis:

proof

take kL ; :: thesis:
thus r < kL by A42, A52, Th5; :: thesis:
upper_bound LEWY <= upper_bound [.r,s.] by A8, SEQ_4:48;
hence kL <= s by A4, A51, JORDAN5A:19; :: thesis:
thus IT . 1 = [.r,kL.[ by A98; :: thesis:

end;

thus ex p being real number st
( r <= p & p < s & IT . (len IT) = ].p,s.] ) :: thesis:

proof

take pP ; :: thesis:
lower_bound [.r,s.] <= lower_bound PRAWY by A8, SEQ_4:47;
hence r <= pP by A4, A70, JORDAN5A:19; :: thesis:
thus pP < s by A68, A71, Th6; :: thesis:
thus IT . (len IT) = ].pP,s.] by A206, A210; :: thesis:

end;

let n be natural number ; :: thesis:
assume A290: ( 1 < n & n < len IT ) ; :: thesis:
consider a, b being Real such that
A291: ( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A215, A290;
take a ; :: thesis:
take b ; :: thesis:
thus ( r <= a & a < b & b <= s & IT . n = ].a,b.[ ) by A290, A291, FINSEQ_4:15; :: thesis:

end;