per cases in F or not [.r,s.] in F ) ;

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

take f = <*[.r,s.]*>; :: thesis:
A6: rng f = {[.r,s.]} by FINSEQ_1:38;
thus rng f c= F by A5, A6, TARSKI:def 1; :: thesis:
thus union (rng f) = [.r,s.] by A6, 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 st
( r < p & p <= s & f . 1 = [.r,p.[ ) & ex p being Real 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 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 :: thesis:

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 real-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;
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;
reconsider Y = X as Subset of REAL by A8, 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 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 object ; :: 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 object ; :: 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;
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, Th47, 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;
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;

A37: now :: thesis:

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

suppose ex a being Real 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 st
( r <= a & a < s & R2 = ].a,s.] ) ; :: thesis:

then consider a being Real such that
r <= a and
a < s and
A38: R2 = ].a,s.] ;
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 st
( r <= a & a < b & b <= s & R2 = ].a,b.[ ) ; :: thesis:

end;

A39: now :: thesis:

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

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

then consider a being Real such that
r < a and
a <= s and
A40: R1 = [.r,a.[ ;
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 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 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 object ; :: according to TARSKI:def 3 :: thesis:
reconsider aa = a as set by TARSKI:1;
assume a in F ; :: thesis:
then aa 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;
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 ;
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 :: thesis:

consider x being object 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 ;
then A49: {} c< g by A47;
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;

A59: now :: thesis:

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

per cases by A60;

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

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

end;

suppose ex a, b being Real 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;
then consider ak being Real such that
A61: r < ak and
ak <= s and
A62: A = [.r,ak.[ by A4, A7, A56, A58, A59, Th44;
A63: A c= LEWY

proof

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

end;

assume A <> LEWY ; :: thesis:
then A c< LEWY by A63;
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 ;
set PRAWY = ].pP,s.];
pP in RM by XXREAL_2:def 7;
then consider b being Real such that
A67: pP = lower_bound ].b,s.] and
A68: ].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 ) ) } ;
A69: lower_bound ].pP,s.] = pP by A45, A67, A68, Th6, XXREAL_1:26;
A70: b < s by A45, A68, XXREAL_1:26;
then pP < s by A67, Th6;
then A71: upper_bound ].pP,s.] = s by Th7;
reconsider PRAWY = ].pP,s.] as non empty Subset of (Closed-Interval-TSpace (r,s)) by A45, A67, A68, Th6, XXREAL_1:26;
A72: pP = b by A45, A67, A68, Th6, XXREAL_1:26;
A73: 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
A74: 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
A75: A <> LEWY and
A76: A <> PRAWY ; :: thesis:
A77: ( A in F & A is open & A is connected ) by A3, A2, A15, A74;

per cases by A4, A7, A45, A74, A77, Th44;

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

then consider a being Real such that
r < a and
a <= s and
A78: A = [.r,a.[ ;

per cases ;

suppose a <= kL ; :: thesis:

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

end;

suppose a > kL ; :: thesis:

then LEWY c= A by A78, XXREAL_1:38;
then LEWY c< A by A75;
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, A74;
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 st
( r <= a & a < s & A = ].a,s.] ) ; :: thesis:

then consider a being Real such that
r <= a and
a < s and
A79: A = ].a,s.] ;

per cases ;

suppose a >= pP ; :: thesis:

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

end;

suppose a < pP ; :: thesis:

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

end;

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

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

end;

A82: 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
A83: 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
A84: upper_bound A in A and
A85: A <> PRAWY ; :: thesis:
A <> LEWY by A51, A84, XXREAL_1:3;
then consider a, b being Real such that
A86: a < b and
A87: A = ].a,b.[ by A73, A83, A85;
upper_bound A = b by A86, A87, TOPREAL6:17;
hence contradiction by A84, A87, 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 );
A88: X c= F by A15, A26;
A89: 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 A90: 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, A88, A90, Th43; :: thesis:

end;

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

end;

consider IT being FinSequence of X such that
A96: len IT = card X and
A97: ( IT . 1 = LLEWY or card X = 0 ) and
A98: for n being Nat st 1 <= n & n < card X holds
S₂[n,IT . n,IT . (n + 1)] from RECDEF_1:sch 4(A91);
A99: 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;
A100: not IT is empty by A96;
then A101: not rng IT is empty ;
then A102: 1 in dom IT by FINSEQ_3:32;
then A103: IT /. 1 = IT . 1 by PARTFUN1:def 6;
A104: 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 A99; :: thesis:

end;

A105: 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 ) ) } ) by A104, A26;
A106: 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 ) );
A107: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

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

per cases by A109, TOPREALA:2;

suppose A112: n = 0 ; :: thesis:

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

end;

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

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

per cases by XXREAL_0:1;

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

then consider j being Nat such that
A119: j in dom IT and
A120: j <= n and
A121: x in IT /. j by A108, A113;
take j ; :: thesis:
thus j in dom IT by A119; :: thesis:
j + 0 < n + 1 by A120, XREAL_1:8;
hence j <= n + 1 ; :: thesis:
thus x in IT /. j by A121; :: thesis:

end;

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

take n + 1 ; :: thesis:
thus n + 1 in dom IT by A109; :: thesis:
thus n + 1 <= n + 1 ; :: thesis:
thus x in IT /. (n + 1) by A110, A113, A115, A122, PARTFUN1:def 6; :: thesis:

end;

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

take n + 1 ; :: thesis:
thus n + 1 in dom IT by A109; :: thesis:
thus n + 1 <= n + 1 ; :: thesis:
lower_bound (IT /. (n + 1)) < x by A117, A123, XXREAL_0:2;
hence x in IT /. (n + 1) by A111, A118, Th30; :: thesis:

end;

A124: S₃[ 0 ] by FINSEQ_3:24;
A125: for n being Nat holds S₃[n] from NAT_1:sch 2(A124, A107);
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 A125; :: thesis:

end;

A126: s in ].b,s.] by A70, XXREAL_1:2;
A127: 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 A128: 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 ) ) );
A129: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

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

per cases by A131, TOPREALA:2;

suppose n = 0 ; :: thesis:

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

end;

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

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

per cases by A134, XXREAL_0:1;

suppose i < n ; :: thesis:

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

per cases by A151, XXREAL_0:1;

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

end;

suppose A160: 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, A82, A132, A148, A141, A160;
hence y1 in IT /. (n + 1) by A70, A72, 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 A155, A156, XXREAL_0:2;
hence x < y1 by A140, XXREAL_0:2; :: thesis:

end;

suppose A161: i = n ; :: thesis:

reconsider y1 = upper_bound (IT /. n) as Element of (Closed-Interval-TSpace (r,s)) by A8, A137, A139, Th2;
take y1 ; :: thesis:
thus y1 in IT /. (n + 1) by A132, A135, A147, A148, PARTFUN1:def 6; :: thesis:
let x be Point of (Closed-Interval-TSpace (r,s)); :: thesis:
assume A162: x in IT /. i ; :: thesis:

A163: now :: thesis:

set IT1 = IT | (Seg n);
A164: 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 object ; :: according to TARSKI:def 3 :: thesis:
assume A in rng (IT | (Seg n)) ; :: thesis:
then A in rng IT by A164;
then A in X by A99;
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 A165: IT /. n = PRAWY by A26, A82, A136, A161, A162;

A166: 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 object ; :: 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
A167: j in dom IT and
A168: j <= n and
A169: l in IT /. j by A106, A135;
1 <= j by A167, FINSEQ_3:25;
then j in Seg n by A168, FINSEQ_1:1;
then A170: IT . j in FI by A167, FUNCT_1:50;
IT . j = IT /. j by A167, PARTFUN1:def 6;
hence l in union FI by A169, A170, TARSKI:def 4; :: thesis:

end;

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

n in Seg n by A142, FINSEQ_1:1;
then A172: IT . n in FI by A135, FUNCT_1:50;
l <= s by A8, XXREAL_1:1;
then l = s by A71, A165, A171, XXREAL_0:1;
hence l in union FI by A72, A126, A138, A165, A172, TARSKI:def 4; :: thesis:

end;

end;

Seg n c= dom IT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A177: n + 0 <= n + 1 by XREAL_1:6;
assume A178: x in Seg n ; :: thesis:
then reconsider x = x as Nat ;
x <= n by A178, FINSEQ_1:1;
then x <= n + 1 by A177, XXREAL_0:2;
then A179: x <= len IT by A146, XXREAL_0:2;
1 <= x by A178, FINSEQ_1:1;
hence x in dom IT by A179, 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 A96, A146, A166, XXREAL_0:2;
hence contradiction by XREAL_1:6; :: thesis:

end;

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

end;

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

A181: IT is one-to-one

proof

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

per cases by A185, 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 A127, A182;
hence contradiction by A183, A184; :: 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 A127, A182;
hence contradiction by A183, A184; :: thesis:

end;

A186: 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
A187: ( i in dom IT & j in dom IT ) and
A188: i <> j ; :: thesis:
( IT /. i = IT . i & IT /. j = IT . j ) by A187, PARTFUN1:def 6;
hence IT /. i <> IT /. j by A181, A187, A188; :: thesis:

end;

A189: 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
A190: s in A and
A191: 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:
A192: ( A in F & A is open ) by A2, A15, A191;

A193: now :: thesis:

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

per cases by A194;

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

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

end;

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

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

end;

A is connected by A3, A15, A191;
then consider ak being Real such that
r <= ak and
A195: ak < s and
A196: A = ].ak,s.] by A4, A7, A190, A192, A193, Th44;
A197: A c= PRAWY

proof

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

end;

assume A <> PRAWY ; :: thesis:
then A c< PRAWY by A197;
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, A68, A72, A191;
hence contradiction by A191, XBOOLE_0:def 5; :: thesis:

end;

take IT ; :: thesis:
thus rng IT c= F by A88, A99; :: thesis:
dom IT = Seg (len IT) by FINSEQ_1:def 3;
then A201: card (dom IT) = card X by A96, FINSEQ_1:57;
reconsider IT1 = IT as Function of (dom IT),X by A99, FUNCT_2:2;
IT1 is onto by A201, A181, FINSEQ_4:63;
then A202: rng IT = X ;
hence union (rng IT) = [.r,s.] by A8, A27; :: 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, A189;
then consider i being object such that
A203: i in dom IT and
A204: IT . i = PRAWY by A202, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A203;
A205: i <= len IT by A203, FINSEQ_3:25;
A206: IT /. i = IT . i by A203, PARTFUN1:def 6;
A207: 1 <= i by A203, FINSEQ_3:25;

A208: now :: thesis:

assume i <> len IT ; :: thesis:
then A209: i < len IT by A205, XXREAL_0:1;
then A210: ex S being Element of X st
( S = IT . i & upper_bound S in IT . (i + 1) ) by A96, A98, A207;
( 0 + 1 <= i + 1 & i + 1 <= len IT ) by A209, NAT_1:13;
then A211: 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 A105, PARTFUN1:def 6;
then i + 0 = i + 1 by A71, A189, A186, A203, A204, A206, A210, A211;
hence contradiction ; :: thesis:

end;

A212: len IT in dom IT by A100, FINSEQ_5:6;
A213: 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
A214: 1 < n and
A215: n < len IT ; :: thesis:
A216: n in dom IT by A214, A215, FINSEQ_3:25;
then IT . n in rng IT by FUNCT_1:def 3;
then A217: IT /. n in rng IT by A216, PARTFUN1:def 6;
then A218: IT /. n in X by A99;
then A219: ( 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, A88;
A220: IT /. n is open connected Subset of (Closed-Interval-TSpace (r,s)) by A89, A99, A217;

per cases by A4, A7, A45, A219, A220, Th44;

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

then consider a being Real such that
A221: r < a and
a <= s and
A222: IT /. n = [.r,a.[ ;
r in [.r,a.[ by A221, XXREAL_1:3;
hence ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A26, A55, A97, A102, A103, A186, A214, A216, A218, A222; :: thesis:

end;

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

then consider a being Real such that
r <= a and
A223: a < s and
A224: IT /. n = ].a,s.] ;
( upper_bound ].a,s.] = s & s in ].a,s.] ) by A223, Th7, XXREAL_1:2;
hence ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A26, A82, A212, A186, A204, A206, A208, A215, A216, A218, A224; :: thesis:

end;

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

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

end;

A226: now :: thesis:

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

end;

hereby :: thesis:

assume A228: n + 1 <= len IT ; :: thesis:
then A229: m < len IT by NAT_1:13;
then A230: IT /. n = IT . n by A227, FINSEQ_4:15;
A231: m in dom IT by A227, A229, FINSEQ_3:25;
then IT /. n in rng IT by A230, FUNCT_1:def 3;
then A232: IT /. n in X by A99;
then A233: 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;
A234: IT /. n is non empty real-bounded interval Subset of REAL by A9, A45, A16, A26, A232;
A235: ex S being Element of X st
( S = IT . n & upper_bound S in IT . (n + 1) ) by A96, A98, A227, A229;
A236: 1 < m + 1 by A227, NAT_1:13;
then A237: IT /. (m + 1) = IT . (m + 1) by A228, FINSEQ_4:15;
A238: n + 1 in dom IT by A228, A236, FINSEQ_3:25;
then A239: IT /. (n + 1) in rng IT by A237, FUNCT_1:def 3;
then A240: IT /. (n + 1) in X by A99;
then A241: 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 A242: IT /. n <> IT /. (n + 1) by A186, A231, A238;
A243: IT /. (n + 1) is non empty real-bounded interval Subset of REAL by A9, A45, A16, A26, A240;
IT /. (n + 1) c= union X by A99, A239, ZFMISC_1:74;
then IT /. (n + 1) c= [.r,s.] by A8, A27;
then A244: IT /. (n + 1) is bounded_above by XXREAL_2:43;
then A245: upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) by A235, A230, A237, SEQ_4:def 1;

hereby :: thesis:

assume A246: 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, A82, A212, A186, A204, A206, A208, A229, A231, A232;
then IT /. n c= IT /. (n + 1) by A234, A243, A245, A246, Th31;
then IT /. n c< IT /. (n + 1) by A242;
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, A233, A241;
hence contradiction by A26, A232, XBOOLE_0:def 5; :: thesis:

end;

thus upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) by A235, A230, A237, A244, SEQ_4:def 1; :: thesis:

per cases by A228, XXREAL_0:1;

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

then pP < upper_bound (IT /. n) by A204, A208, A235, A230, XXREAL_1:2;
hence lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) by A204, A206, A208, A247, Th6, XXREAL_1:26; :: thesis:

end;

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

then consider a1, b1 being Real such that
r <= a1 and
A248: a1 < b1 and
b1 <= s and
A249: IT /. (n + 1) = ].a1,b1.[ by A213, A236;
a1 < upper_bound (IT /. n) by A235, A230, A237, A249, XXREAL_1:4;
hence lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) by A248, A249, TOPREAL6:17; :: thesis:

end;

hereby :: thesis:

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

proof

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

per cases ;

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

per cases ;

suppose A270: n = 1 ; :: thesis:

then lower_bound (IT /. n) <= x by A8, A53, A97, A103, A258, A266, XXREAL_1:1;
then x in IT /. n by A42, A54, A53, A97, A103, A269, A270, XXREAL_1:3;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

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

n + 0 < n + 2 by XREAL_1:6;
then A272: n < len IT by A254, XXREAL_0:2;
A273: lower_bound (IT /. n) < x by A251, A255, A262, A263, A267, NAT_1:13, XXREAL_0:2;
1 < n by A250, A271, XXREAL_0:1;
then consider a, b being Real such that
r <= a and
A274: a < b and
b <= s and
A275: IT /. n = ].a,b.[ by A213, A272;
( lower_bound (IT /. n) = a & upper_bound (IT /. n) = b ) by A274, A275, TOPREAL6:17;
then x in IT /. n by A269, A275, A273, 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 A276: x > lower_bound (IT /. (n + 2)) by A260, XXREAL_0:2;

per cases ;

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

x <= s by A8, A258, A266, XXREAL_1:1;
then x in IT /. (n + 2) by A69, A204, A206, A208, A276, A277, XXREAL_1:2;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

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

n + 1 < n + 2 by XREAL_1:6;
then A279: 1 < n + 2 by A253, XXREAL_0:2;
(n + 1) + 1 < len IT by A254, A278, XXREAL_0:1;
then consider a2, b2 being Real such that
r <= a2 and
A280: a2 < b2 and
b2 <= s and
A281: IT /. (n + 2) = ].a2,b2.[ by A213, A279;
upper_bound ].a2,b2.[ = b2 by A280, TOPREAL6:17;
then A282: x < b2 by A259, A262, A264, A268, A281, XXREAL_0:2;
lower_bound ].a2,b2.[ = a2 by A280, TOPREAL6:17;
then x in IT /. (n + 2) by A276, A281, A282, 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 A253, XXREAL_0:2;
then A283: m + 2 in dom IT by A254, FINSEQ_3:25;
then IT /. (n + 2) = IT . (n + 2) by PARTFUN1:def 6;
then IT /. (n + 2) in rng IT by A283, FUNCT_1:def 3;
then A284: IT /. (n + 2) in X by A99;
m <= len IT by A252, A256, XXREAL_0:2;
then A285: n in dom IT by A250, FINSEQ_3:25;
then IT /. n = IT . n by PARTFUN1:def 6;
then IT /. n in rng IT by A285, FUNCT_1:def 3;
then A286: IT /. n in X by A99;
n + 1 < n + 2 by XREAL_1:6;
then A287: IT /. (n + 2) <> IT /. (n + 1) by A186, A257, A283;
n + 0 < n + 1 by XREAL_1:6;
then IT /. n <> IT /. (n + 1) by A186, A285, A257;
hence contradiction by A22, A24, A286, A258, A284, A287, A265, Th48; :: 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 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 A97; :: thesis:

end;

thus ex p being Real 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, A69, JORDAN5A:19; :: thesis:
thus pP < s by A67, A70, Th6; :: thesis:
thus IT . (len IT) = ].pP,s.] by A204, A208; :: thesis:

end;

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

end;