take f = <*[.r,s.]*>; :: thesis:
A2: 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 A1, A2, TARSKI:def 1; :: thesis:

end;

thus union (rng f) = [.r,s.] by A2, ZFMISC_1:25; :: thesis:
thus ( ( for n being Nat 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 Nat 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 B4, A1, Lm3; :: thesis:

end;

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

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

A5: now :: thesis:

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

end;

Closed-Interval-TSpace (r,s) is compact by B4, 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
A6: G c= F and
A7: G is Cover of [#] (Closed-Interval-TSpace (r,s)) and
A8: G is finite by B1, B2, 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 ) ) } ) } ;
A9: 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 ) ) } } ;
A10: 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 A11: 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 A6, XBOOLE_1:1;
A12: 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 B3, A11, Def1;
reconsider Y = X as Subset of REAL by A4, XBOOLE_1:1;
Y is interval by Th43;
hence X is interval Subset of REAL ; :: thesis:

end;

reconsider T = Closed-Interval-TSpace (r,s) as non empty connected TopSpace by B4, 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 ) ) } } ;
A13: { (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;

A14: { (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 ) ) } } ;
A15: { (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;

A16: { (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;

A17: 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 A9, ORDERS_1:def 7;
then consider M being set such that
A18: 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 A7, A8, A17, Th47, ORDERS_1:64;
A19: 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 A18, ORDERS_1:def 12;
then consider C being Subset-Family of (Closed-Interval-TSpace (r,s)) such that
A20: M = C and
A21: C is Cover of (Closed-Interval-TSpace (r,s)) and
A22: 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 A17;
A23: union C = [#] (Closed-Interval-TSpace (r,s)) by A21, SETFAM_1:45;
A24: s in [.r,s.] by B4, XXREAL_1:1;
then consider R2 being set such that
A25: s in R2 and
A26: R2 in C by A4, A23, TARSKI:def 4;
r in [.r,s.] by B4, XXREAL_1:1;
then consider R1 being set such that
A27: r in R1 and
A28: R1 in C by A4, A23, TARSKI:def 4;
A29: 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 A22, A28;
then A30: R1 in F by A11;
A31: 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 A22, A26;
then A32: R2 in F by A11;
reconsider R1 = R1, R2 = R2 as open connected Subset of (Closed-Interval-TSpace (r,s)) by B2, B3, A11, A29, A31, Def1, TOPS_2:def 1;

A33: now :: thesis:

per cases by B4, A3, A25, A32, Th44;

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 A25, 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
A34: 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 A22, A26, A34;
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;

A35: now :: thesis:

per cases by B4, A3, A27, A30, Th44;

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
A36: 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 A22, A28, A36;
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 A27, XXREAL_1:2; :: thesis:

end;

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

end;

A37: 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 A8;
{ (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(A37);
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 A15, A33, A16;
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 A4, 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 A11, XBOOLE_1:1;
then reconsider X = C as non empty finite Subset-Family of REAL by A8, A22, A28, 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(A37);
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 A13, A35, A14;
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
A38: kL = upper_bound [.r,b.[ and
A39: [.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 ) ) } ;
A40: union G = [#] (Closed-Interval-TSpace (r,s)) by A7, SETFAM_1:45;

A41: now :: thesis:

consider x being set such that
A42: x in the carrier of (Closed-Interval-TSpace (r,s)) by XBOOLE_0:def 1;
consider g being set such that
A43: x in g and
A44: g in G by A40, A42, TARSKI:def 4;
{} c= g by XBOOLE_1:2;
then A45: {} c< g by A43, XBOOLE_0:def 8;
assume A46: {} 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 A44, A45;
hence contradiction by A46, XBOOLE_0:def 5; :: thesis:

end;

then A47: upper_bound [.r,kL.[ = kL by A38, A39, Th5, XXREAL_1:27;
A48: r < b by A41, A39, XXREAL_1:27;
then r < kL by A38, Th5;
then A49: lower_bound [.r,kL.[ = r by Th4;
reconsider LEWY = [.r,kL.[ as non empty Subset of (Closed-Interval-TSpace (r,s)) by A41, A38, A39, Th5, XXREAL_1:27;
A50: kL = b by A41, A38, A39, Th5, XXREAL_1:27;
A51: 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
A52: r in A and
A53: 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:
A54: ( A in F & A is open ) by B2, A11, A53, TOPS_2:def 1;

A55: now :: thesis:

assume A56: ( 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 A56;

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

hence contradiction by A52, 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 A52, XXREAL_1:4; :: thesis:

end;

A is connected by B3, A11, A53, Def1;
then consider ak being real number such that
A57: r < ak and
ak <= s and
A58: A = [.r,ak.[ by B4, A3, A52, A54, A55, Th44;
A59: ak is Real by XREAL_0:def 1;
A60: A c= LEWY

proof

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

end;

assume A <> LEWY ; :: thesis:
then A c< LEWY by A60, 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 A10, A39, A50, A53;
hence contradiction by A53, XBOOLE_0:def 5; :: thesis:

end;

then reconsider LLEWY = LEWY as Element of X by A22, A27, A28;
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
A64: pP = lower_bound ].b,s.] and
A65: ].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 ) ) } ;
A66: lower_bound ].pP,s.] = pP by A41, A64, A65, Th6, XXREAL_1:26;
A67: b < s by A41, A65, XXREAL_1:26;
then pP < s by A64, Th6;
then A68: upper_bound ].pP,s.] = s by Th7;
reconsider PRAWY = ].pP,s.] as non empty Subset of (Closed-Interval-TSpace (r,s)) by A41, A64, A65, Th6, XXREAL_1:26;
A69: pP = b by A41, A64, A65, Th6, XXREAL_1:26;
A70: 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
A71: 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
A72: A <> LEWY and
A73: A <> PRAWY ; :: thesis:
A74: ( A in F & A is open & A is connected ) by B3, B2, A11, A71, Def1, TOPS_2:def 1;

per cases by B4, A3, A41, A71, A74, Th44;

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
A75: A = [.r,a.[ ;

per cases ;

suppose a <= kL ; :: thesis:

then A c= LEWY by A75, XXREAL_1:38;
then A c< LEWY by A72, 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 A10, A39, A50, A71;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A71, XBOOLE_0:def 5; :: thesis:

end;

suppose a > kL ; :: thesis:

then LEWY c= A by A75, XXREAL_1:38;
then LEWY c< A by A72, 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 A10, A39, A50, A71;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A39, A50, 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
A76: A = ].a,s.] ;

per cases ;

suppose a >= pP ; :: thesis:

then A c= PRAWY by A76, XXREAL_1:42;
then A c< PRAWY by A73, 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 A10, A65, A69, A71;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A71, XBOOLE_0:def 5; :: thesis:

end;

suppose a < pP ; :: thesis:

then PRAWY c= A by A76, XXREAL_1:42;
then PRAWY c< A by A73, 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 A10, A65, A69, A71;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A65, A69, 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
A77: a < b and
b <= s and
A78: 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 A77, A78; :: thesis:

end;

A79: 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
A80: 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
A81: upper_bound A in A and
A82: A <> PRAWY ; :: thesis:
A <> LEWY by A47, A81, XXREAL_1:3;
then consider a, b being Real such that
A83: a < b and
A84: A = ].a,b.[ by A70, A80, A82;
upper_bound A = b by A83, A84, TOPREAL6:17;
hence contradiction by A81, A84, 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 );
A85: X c= F by A11, A22, XBOOLE_1:1;
A86: 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 A87: Z in X ; :: thesis:
then ( not Z is empty & Z is interval ) by A41, A12, A22;
hence Z is non empty open connected Subset of T by B2, A85, A87, Th43, TOPS_2:def 1; :: thesis:

end;

A88: 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 ;
A89: not x1 is empty by A86;
A90: x c= union X by ZFMISC_1:74;
then x c= [.r,s.] by A4, A23;
then x1 is bounded_above by XXREAL_2:43;
then upper_bound x is Element of (Closed-Interval-TSpace (r,s)) by A4, A23, A89, A90, Th2;
then consider y being set such that
A91: upper_bound x in y and
A92: y in X by A23, TARSKI:def 4;
reconsider y = y as Element of X by A92;
take y ; :: thesis:
take x ; :: thesis:
thus ( x = x & upper_bound x in y ) by A91; :: thesis:

end;

consider IT being FinSequence of X such that
A93: len IT = card X and
A94: ( IT . 1 = LLEWY or card X = 0 ) and
A95: 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(A88);
A96: 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;
A97: not IT is empty by A93;
then A98: not rng IT is empty ;
then A99: 1 in dom IT by FINSEQ_3:32;
then A100: IT /. 1 = IT . 1 by PARTFUN1:def 6;
A101: for n being Nat st n in dom IT holds
( IT . n in X & IT /. n in X )

proof

let n be Nat; :: 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 A96; :: thesis:

end;

A102: for n being Nat 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 Nat; :: thesis:
assume n in dom IT ; :: thesis:
then ( IT . n = IT /. n & IT . n in X ) by A101, 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 A22; :: thesis:

end;

A103: for i being Nat 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 Nat st
( j in dom IT & j <= i & x in IT /. j )

proof

defpred S₃[ Nat] 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 Nat st
( j in dom IT & j <= $1 & x in IT /. j ) );
A104: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

let n be Nat; :: thesis:
assume that
A105: S₃[n] and
A106: n + 1 in dom IT ; :: thesis:
A107: IT /. (n + 1) = IT . (n + 1) by A106, PARTFUN1:def 6;
let x be Point of (Closed-Interval-TSpace (r,s)); :: thesis:
assume A108: x < upper_bound (IT /. (n + 1)) ; :: thesis:

per cases by A106, TOPREALA:2;

suppose A109: n = 0 ; :: thesis:

take 1 ; :: thesis:
thus 1 in dom IT by A98, FINSEQ_3:32; :: thesis:
thus 1 <= n + 1 by A109; :: thesis:
r <= x by A4, XXREAL_1:1;
hence x in IT /. 1 by A47, A94, A108, A107, A109, XXREAL_1:3; :: thesis:

end;

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

n + 1 <= len IT by A106, FINSEQ_3:25;
then A111: n < len IT by NAT_1:13;
1 <= n by A110, FINSEQ_3:25;
then A112: ex S being Element of X st
( S = IT . n & upper_bound S in IT . (n + 1) ) by A93, A95, A110, A111;
IT /. (n + 1) in X by A101, A106;
then A113: IT /. (n + 1) is bounded_below by A5;
IT /. n = IT . n by A110, PARTFUN1:def 6;
then A114: lower_bound (IT /. (n + 1)) <= upper_bound (IT /. n) by A107, A113, A112, SEQ_4:def 2;
A115: ( IT /. (n + 1) is interval Subset of REAL & not IT /. (n + 1) is empty ) by A41, A12, A102, A106;

per cases by XXREAL_0:1;

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

then consider j being Nat such that
A116: j in dom IT and
A117: j <= n and
A118: x in IT /. j by A105, A110;
take j ; :: thesis:
thus j in dom IT by A116; :: thesis:
j + 0 < n + 1 by A117, XREAL_1:8;
hence j <= n + 1 ; :: thesis:
thus x in IT /. j by A118; :: thesis:

end;

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

take n + 1 ; :: thesis:
thus n + 1 in dom IT by A106; :: thesis:
thus n + 1 <= n + 1 ; :: thesis:
thus x in IT /. (n + 1) by A107, A110, A112, A119, PARTFUN1:def 6; :: thesis:

end;

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

take n + 1 ; :: thesis:
thus n + 1 in dom IT by A106; :: thesis:
thus n + 1 <= n + 1 ; :: thesis:
lower_bound (IT /. (n + 1)) < x by A114, A120, XXREAL_0:2;
hence x in IT /. (n + 1) by A108, A115, Th30; :: thesis:

end;

A121: S₃[ 0 ] by FINSEQ_3:24;
A122: for n being Nat holds S₃[n] from NAT_1:sch 2(A121, A104);
let i be Nat; :: 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 Nat st
( j in dom IT & j <= i & x in IT /. j ) by A122; :: thesis:

end;

A123: s in ].b,s.] by A67, XXREAL_1:2;
A124: for i being Nat st i in dom IT holds
for j being Nat 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 Nat; :: thesis:
assume A125: i in dom IT ; :: thesis:
defpred S₃[ Nat] 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 ) ) );
A126: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

let n be Nat; :: thesis:
assume that
A127: S₃[n] and
A128: n + 1 in dom IT ; :: thesis:
A129: IT /. (n + 1) = IT . (n + 1) by A128, PARTFUN1:def 6;
assume A130: i < n + 1 ; :: thesis:
then A131: i <= n by NAT_1:13;

per cases by A128, TOPREALA:2;

suppose n = 0 ; :: thesis:

then i = 0 by A130, 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 A125, FINSEQ_3:24; :: thesis:

end;

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

then A133: IT /. n in X by A101;
then A134: IT /. n is bounded_above by A5;
A135: IT /. n = IT . n by A132, PARTFUN1:def 6;
then IT /. n in rng IT by A132, FUNCT_1:def 3;
then A136: ( not IT /. n is empty & IT /. n is Subset of (Closed-Interval-TSpace (r,s)) ) by A86, A96;
then upper_bound (IT /. n) in [.r,s.] by A4, A134, Th2;
then A137: upper_bound (IT /. n) <= s by XXREAL_1:1;
A138: IT /. (n + 1) in X by A101, A128;
A139: 1 <= n by A132, FINSEQ_3:25;
A140: IT /. (n + 1) in rng IT by A128, A129, FUNCT_1:def 3;
then A141: IT /. (n + 1) is open connected Subset of (Closed-Interval-TSpace (r,s)) by A86, A96;
then A142: IT /. (n + 1) is interval Subset of REAL by Th43;
A143: n + 1 <= len IT by A128, FINSEQ_3:25;
then ( n is Element of NAT & n < card X ) by A93, NAT_1:13, ORDINAL1:def 12;
then consider S being Element of X such that
A144: S = IT . n and
A145: upper_bound S in IT . (n + 1) by A95, A139;
IT /. (n + 1) is bounded_below by A5, A141;
then A146: lower_bound (IT /. (n + 1)) <= upper_bound S by A129, A145, SEQ_4:def 2;
A147: IT /. (n + 1) is bounded_above by A5, A141;
then A148: upper_bound S <= upper_bound (IT /. (n + 1)) by A129, A145, SEQ_4:def 1;
A149: not IT /. (n + 1) is empty by A86, A96, A140;
then upper_bound (IT /. (n + 1)) in [.r,s.] by A4, A141, A147, Th2;
then A150: upper_bound (IT /. (n + 1)) <= s by XXREAL_1:1;

per cases by A131, XXREAL_0:1;

suppose i < n ; :: thesis:

then consider y being Point of (Closed-Interval-TSpace (r,s)) such that
A151: y in IT /. n and
A152: for x being Point of (Closed-Interval-TSpace (r,s)) st x in IT /. i holds
x < y by A127, A132;
A153: y <= upper_bound (IT /. n) by A134, A151, SEQ_4:def 1;

per cases by A148, XXREAL_0:1;

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

end;

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

reconsider y1 = s as Point of (Closed-Interval-TSpace (r,s)) by B4, A4, XXREAL_1:1;
take y1 ; :: thesis:
IT /. (n + 1) = PRAWY by A22, A79, A129, A145, A138, A157;
hence y1 in IT /. (n + 1) by A67, A69, 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 A152, A153, XXREAL_0:2;
hence x < y1 by A137, XXREAL_0:2; :: thesis:

end;

suppose A158: i = n ; :: thesis:

reconsider y1 = upper_bound (IT /. n) as Element of (Closed-Interval-TSpace (r,s)) by A4, A134, A136, Th2;
take y1 ; :: thesis:
thus y1 in IT /. (n + 1) by A129, A132, A144, A145, PARTFUN1:def 6; :: thesis:
let x be Point of (Closed-Interval-TSpace (r,s)); :: thesis:
assume A159: x in IT /. i ; :: thesis:

A160: now :: thesis:

set IT1 = IT | (Seg n);
A161: 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 A161;
then A in X by A96;
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 A162: IT /. n = PRAWY by A22, A79, A133, A158, A159;

A163: now :: thesis:

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 Nat such that
A164: j in dom IT and
A165: j <= n and
A166: l in IT /. j by A103, A132;
1 <= j by A164, FINSEQ_3:25;
then j in Seg n by A165, FINSEQ_1:1;
then A167: IT . j in FI by A164, FUNCT_1:50;
IT . j = IT /. j by A164, PARTFUN1:def 6;
hence l in union FI by A166, A167, TARSKI:def 4; :: thesis:

end;

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

n in Seg n by A139, FINSEQ_1:1;
then A169: IT . n in FI by A132, FUNCT_1:50;
l <= s by A4, XXREAL_1:1;
then l = s by A68, A162, A168, XXREAL_0:1;
hence l in union FI by A69, A123, A135, A162, A169, TARSKI:def 4; :: thesis:

end;

end;

Seg n c= dom IT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
A174: n + 0 <= n + 1 by XREAL_1:6;
assume A175: x in Seg n ; :: thesis:
then reconsider x = x as Nat ;
x <= n by A175, FINSEQ_1:1;
then x <= n + 1 by A174, XXREAL_0:2;
then A176: x <= len IT by A143, XXREAL_0:2;
1 <= x by A175, FINSEQ_1:1;
hence x in dom IT by A176, 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 A93, A143, A163, XXREAL_0:2;
hence contradiction by XREAL_1:6; :: thesis:

end;

x <= upper_bound (IT /. n) by A134, A158, A159, SEQ_4:def 1;
hence x < y1 by A160, XXREAL_0:1; :: thesis:

end;

A177: S₃[ 0 ] ;
for n being Nat holds S₃[n] from NAT_1:sch 2(A177, A126);
hence for j being Nat 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;

A178: IT is one-to-one

proof

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

per cases by A182, 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 A124, A179;
hence contradiction by A180, A181; :: 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 A124, A179;
hence contradiction by A180, A181; :: thesis:

end;

A183: for i, j being Nat st i in dom IT & j in dom IT & i <> j holds
IT /. i <> IT /. j

proof

let i, j be Nat; :: thesis:
assume that
A184: ( i in dom IT & j in dom IT ) and
A185: i <> j ; :: thesis:
( IT /. i = IT . i & IT /. j = IT . j ) by A184, PARTFUN1:def 6;
hence IT /. i <> IT /. j by A178, A184, A185, FUNCT_1:def 4; :: thesis:

end;

A186: 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
A187: s in A and
A188: 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:
A189: ( A in F & A is open ) by B2, A11, A188, TOPS_2:def 1;

A190: now :: thesis:

assume A191: ( 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 A191;

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

hence contradiction by A187, 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 A187, XXREAL_1:4; :: thesis:

end;

A is connected by B3, A11, A188, Def1;
then consider ak being real number such that
r <= ak and
A192: ak < s and
A193: A = ].ak,s.] by B4, A3, A187, A189, A190, Th44;
A194: ak is Real by XREAL_0:def 1;
A195: A c= PRAWY

proof

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

end;

assume A <> PRAWY ; :: thesis:
then A c< PRAWY by A195, 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 A10, A65, A69, A188;
hence contradiction by A188, XBOOLE_0:def 5; :: thesis:

end;

take IT ; :: thesis:
thus rng IT c= F by A85, A96, XBOOLE_1:1; :: thesis:
dom IT = Seg (len IT) by FINSEQ_1:def 3;
then A199: card (dom IT) = card X by A93, FINSEQ_1:57;
IT is Function of (dom IT),X by A96, FUNCT_2:2;
then A200: rng IT = X by A199, A178, FINSEQ_4:63;
hence union (rng IT) = [.r,s.] by A4, A23; :: thesis:
ex Z being set st
( s in Z & Z in C ) by A24, A4, A23, TARSKI:def 4;
then PRAWY in X by A22, A186;
then consider i being set such that
A201: i in dom IT and
A202: IT . i = PRAWY by A200, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A201;
A203: i <= len IT by A201, FINSEQ_3:25;
A204: IT /. i = IT . i by A201, PARTFUN1:def 6;
A205: 1 <= i by A201, FINSEQ_3:25;

A206: now :: thesis:

assume i <> len IT ; :: thesis:
then A207: i < len IT by A203, XXREAL_0:1;
then A208: ex S being Element of X st
( S = IT . i & upper_bound S in IT . (i + 1) ) by A93, A95, A205;
( 0 + 1 <= i + 1 & i + 1 <= len IT ) by A207, NAT_1:13;
then A209: 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 A102, PARTFUN1:def 6;
then i + 0 = i + 1 by A68, A186, A183, A201, A202, A204, A208, A209;
hence contradiction ; :: thesis:

end;

A210: len IT in dom IT by A97, FINSEQ_5:6;
A211: for n being Nat 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 Nat; :: thesis:
assume that
A212: 1 < n and
A213: n < len IT ; :: thesis:
A214: n in dom IT by A212, A213, FINSEQ_3:25;
then IT . n in rng IT by FUNCT_1:def 3;
then A215: IT /. n in rng IT by A214, PARTFUN1:def 6;
then A216: IT /. n in X by A96;
then A217: ( 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 A22, A85;
A218: IT /. n is open connected Subset of (Closed-Interval-TSpace (r,s)) by A86, A96, A215;

per cases by B4, A3, A41, A217, A218, Th44;

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

then consider a being real number such that
A219: r < a and
a <= s and
A220: IT /. n = [.r,a.[ ;
r in [.r,a.[ by A219, XXREAL_1:3;
hence ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A22, A51, A94, A99, A100, A183, A212, A214, A216, A220; :: 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
A221: a < s and
A222: IT /. n = ].a,s.] ;
( upper_bound ].a,s.] = s & s in ].a,s.] ) by A221, Th7, XXREAL_1:2;
hence ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A22, A79, A210, A183, A202, A204, A206, A213, A214, A216, A222; :: 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
A223: ( 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 A223; :: thesis:

end;

A224: now :: thesis:

let n be Nat; :: thesis:
assume A225: 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 A225, FINSEQ_3:25, FINSEQ_4:15;
then IT /. n in rng IT by FUNCT_1:def 3;
then IT /. n in X by A96;
hence not IT /. n is empty by A41, A22; :: thesis:

end;

hereby :: thesis:

assume A226: n + 1 <= len IT ; :: thesis:
then A227: m < len IT by NAT_1:13;
then A228: IT /. n = IT . n by A225, FINSEQ_4:15;
A229: m in dom IT by A225, A227, FINSEQ_3:25;
then IT /. n in rng IT by A228, FUNCT_1:def 3;
then A230: IT /. n in X by A96;
then A231: 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 A22;
A232: IT /. n is non empty real-bounded interval Subset of REAL by A5, A41, A12, A22, A230;
A233: ex S being Element of X st
( S = IT . n & upper_bound S in IT . (n + 1) ) by A93, A95, A225, A227;
A234: 1 < m + 1 by A225, NAT_1:13;
then A235: IT /. (m + 1) = IT . (m + 1) by A226, FINSEQ_4:15;
A236: n + 1 in dom IT by A226, A234, FINSEQ_3:25;
then A237: IT /. (n + 1) in rng IT by A235, FUNCT_1:def 3;
then A238: IT /. (n + 1) in X by A96;
then A239: 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 A22;
n + 0 < n + 1 by XREAL_1:6;
then A240: IT /. n <> IT /. (n + 1) by A183, A229, A236;
A241: IT /. (n + 1) is non empty real-bounded interval Subset of REAL by A5, A41, A12, A22, A238;
IT /. (n + 1) c= union X by A96, A237, ZFMISC_1:74;
then IT /. (n + 1) c= [.r,s.] by A4, A23;
then A242: IT /. (n + 1) is bounded_above by XXREAL_2:43;
then A243: upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) by A233, A228, A235, SEQ_4:def 1;

hereby :: thesis:

assume A244: 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 A22, A79, A210, A183, A202, A204, A206, A227, A229, A230;
then IT /. n c= IT /. (n + 1) by A232, A241, A243, A244, Th31;
then IT /. n c< IT /. (n + 1) by A240, 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 A10, A231, A239;
hence contradiction by A22, A230, XBOOLE_0:def 5; :: thesis:

end;

thus upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) by A233, A228, A235, A242, SEQ_4:def 1; :: thesis:

per cases by A226, XXREAL_0:1;

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

then pP < upper_bound (IT /. n) by A202, A206, A233, A228, XXREAL_1:2;
hence lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) by A202, A204, A206, A245, Th6, XXREAL_1:26; :: thesis:

end;

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

then consider a1, b1 being Real such that
r <= a1 and
A246: a1 < b1 and
b1 <= s and
A247: IT /. (n + 1) = ].a1,b1.[ by A211, A234;
a1 < upper_bound (IT /. n) by A233, A228, A235, A247, XXREAL_1:4;
hence lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) by A246, A247, TOPREAL6:17; :: thesis:

end;

hereby :: thesis:

let n be Nat; :: thesis:
assume A248: 1 <= n ; :: thesis:
thus A249: ( ( 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 A224, A248; :: thesis:
reconsider m = n as Nat ;
A250: n + 0 < n + 1 by XREAL_1:6;
then A251: 1 < m + 1 by A248, XXREAL_0:2;
assume A252: n + 2 <= len IT ; :: thesis:
then A253: (n + 1) + 1 <= len IT ;
then A254: m + 1 < len IT by NAT_1:13;
then A255: n + 1 in dom IT by A251, FINSEQ_3:25;
then IT /. (n + 1) = IT . (n + 1) by PARTFUN1:def 6;
then IT /. (n + 1) in rng IT by A255, FUNCT_1:def 3;
then A256: IT /. (n + 1) in X by A96;
0 + 1 <= n + 1 by XREAL_1:6;
then A257: upper_bound (IT /. (n + 1)) <= upper_bound (IT /. ((n + 1) + 1)) by A224, A252;
assume A258: upper_bound (IT /. n) > lower_bound (IT /. (n + 2)) ; :: thesis:
consider a1, b1 being Real such that
r <= a1 and
A259: a1 < b1 and
b1 <= s and
A260: IT /. (n + 1) = ].a1,b1.[ by A211, A251, A254;
A261: lower_bound ].a1,b1.[ = a1 by A259, TOPREAL6:17;
A262: upper_bound ].a1,b1.[ = b1 by A259, TOPREAL6:17;
A263: IT /. (n + 1) c= (IT /. n) \/ (IT /. (n + 2))

proof

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

per cases ;

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

per cases ;

suppose A268: n = 1 ; :: thesis:

then lower_bound (IT /. n) <= x by A4, A49, A94, A100, A256, A264, XXREAL_1:1;
then x in IT /. n by A38, A50, A49, A94, A100, A267, A268, XXREAL_1:3;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

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

n + 0 < n + 2 by XREAL_1:6;
then A270: n < len IT by A252, XXREAL_0:2;
A271: lower_bound (IT /. n) < x by A249, A253, A260, A261, A265, NAT_1:13, XXREAL_0:2;
1 < n by A248, A269, XXREAL_0:1;
then consider a, b being Real such that
r <= a and
A272: a < b and
b <= s and
A273: IT /. n = ].a,b.[ by A211, A270;
( lower_bound (IT /. n) = a & upper_bound (IT /. n) = b ) by A272, A273, TOPREAL6:17;
then x in IT /. n by A267, A273, A271, 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 A274: x > lower_bound (IT /. (n + 2)) by A258, XXREAL_0:2;

per cases ;

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

x <= s by A4, A256, A264, XXREAL_1:1;
then x in IT /. (n + 2) by A66, A202, A204, A206, A274, A275, XXREAL_1:2;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

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

n + 1 < n + 2 by XREAL_1:6;
then A277: 1 < n + 2 by A251, XXREAL_0:2;
(n + 1) + 1 < len IT by A252, A276, XXREAL_0:1;
then consider a2, b2 being Real such that
r <= a2 and
A278: a2 < b2 and
b2 <= s and
A279: IT /. (n + 2) = ].a2,b2.[ by A211, A277;
upper_bound ].a2,b2.[ = b2 by A278, TOPREAL6:17;
then A280: x < b2 by A257, A260, A262, A266, A279, XXREAL_0:2;
lower_bound ].a2,b2.[ = a2 by A278, TOPREAL6:17;
then x in IT /. (n + 2) by A274, A279, A280, 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 A251, XXREAL_0:2;
then A281: m + 2 in dom IT by A252, FINSEQ_3:25;
then IT /. (n + 2) = IT . (n + 2) by PARTFUN1:def 6;
then IT /. (n + 2) in rng IT by A281, FUNCT_1:def 3;
then A282: IT /. (n + 2) in X by A96;
m <= len IT by A250, A254, XXREAL_0:2;
then A283: n in dom IT by A248, FINSEQ_3:25;
then IT /. n = IT . n by PARTFUN1:def 6;
then IT /. n in rng IT by A283, FUNCT_1:def 3;
then A284: IT /. n in X by A96;
n + 1 < n + 2 by XREAL_1:6;
then A285: IT /. (n + 2) <> IT /. (n + 1) by A183, A255, A281;
n + 0 < n + 1 by XREAL_1:6;
then IT /. n <> IT /. (n + 1) by A183, A283, A255;
hence contradiction by A18, A19, A20, A284, A256, A282, A285, A263, Th48; :: thesis:

end;

thus ( [.r,s.] in F implies IT = <*[.r,s.]*> ) by A3; :: 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 A38, A48, Th5; :: thesis:
upper_bound LEWY <= upper_bound [.r,s.] by A4, SEQ_4:48;
hence kL <= s by B4, A47, JORDAN5A:19; :: thesis:
thus IT . 1 = [.r,kL.[ by A94; :: 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 A4, SEQ_4:47;
hence r <= pP by B4, A66, JORDAN5A:19; :: thesis:
thus pP < s by A64, A67, Th6; :: thesis:
thus IT . (len IT) = ].pP,s.] by A202, A206; :: thesis:

end;

let n be Nat; :: thesis:
assume A286: ( 1 < n & n < len IT ) ; :: thesis:
consider a, b being Real such that
A287: ( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A211, A286;
take a ; :: thesis:
take b ; :: thesis:
thus ( r <= a & a < b & b <= s & IT . n = ].a,b.[ ) by A286, A287, FINSEQ_4:15; :: thesis:

end;