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:55;
thus rng f c= F :: thesis:

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

end;

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

end;

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

A8: r in [.r,s.] by A4, XXREAL_1:1;
A9: s in [.r,s.] by A4, XXREAL_1:1;
set L = Closed-Interval-TSpace r,s;
A10: the carrier of (Closed-Interval-TSpace r,s) = [.r,s.] by A4, TOPMETR:25;
reconsider T = Closed-Interval-TSpace r,s as non empty connected TopSpace by A4, TREAL_1:23;
A12: F is Cover of [#] (Closed-Interval-TSpace r,s) by A1;
Closed-Interval-TSpace r,s is compact by A4, HEINE:11;
then [#] (Closed-Interval-TSpace r,s) is compact by COMPTS_1:10;
then consider G being Subset-Family of (Closed-Interval-TSpace r,s) such that
A13: G c= F and
A14: G is Cover of [#] (Closed-Interval-TSpace r,s) and
A15: G is finite by A2, A12, COMPTS_1:def 7;
A16: G is Cover of (Closed-Interval-TSpace r,s) by A14;
then A17: union G = [#] (Closed-Interval-TSpace r,s) by SETFAM_1:60;

A18: now

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

end;

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 ) ) } ;
A19: 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;
A20: 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 A15;

A21: now

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

end;

A27: 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 A13, A19, XBOOLE_1:1;
A28: 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 connected 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, A27, Def1;
reconsider Y = X as Subset of REAL by A10, XBOOLE_1:1;
Y is connected by Th56;
hence X is connected Subset of REAL ; :: thesis:

end;

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 A10, XBOOLE_1:1;
hence a in bool REAL ; :: thesis:

end;

then A29: 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 A27, XBOOLE_1:1;
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 ) ) } ) } ;
A30: 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 ) ) } ) }

proof

thus ( 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 ) ) } ) } & 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:29, WELLORD2:30, WELLORD2:31; :: according to ORDERS_1:def 7 :: thesis:

end;

A31: 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;
{ 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 ) ) } ) } has_lower_Zorn_property_wrt 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 A15, A16, Th61;
then consider M being set such that
A32: 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 A30, A31, ORDERS_1:174;
A33: 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 A32, ORDERS_1:def 12;
then consider C being Subset-Family of (Closed-Interval-TSpace r,s) such that
A34: M = C and
A35: C is Cover of (Closed-Interval-TSpace r,s) and
A36: 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 A31;
A37: union C = [#] (Closed-Interval-TSpace r,s) by A35, SETFAM_1:60;
then consider R1 being set such that
A38: r in R1 and
A39: R1 in C by A8, A10, TARSKI:def 4;
consider R2 being set such that
A40: s in R2 and
A41: R2 in C by A9, A10, A37, TARSKI:def 4;
A42: 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 A36, A39;
then A43: R1 in F by A27;
A44: 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 A36, A41;
then A45: R2 in F by A27;
reconsider R1 = R1, R2 = R2 as open connected Subset of (Closed-Interval-TSpace r,s) by A2, A3, A27, A42, A44, Def1, TOPS_2:def 1;
reconsider X = C as non empty finite Subset-Family of REAL by A15, A29, A36, A39, XBOOLE_1:1;
A46: X c= F by A27, A36, XBOOLE_1:1;
A47: 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 A48: Z in X ; :: thesis:
then ( not Z is empty & Z is connected ) by A21, A28, A36;
hence Z is non empty open connected Subset of T by A2, A46, A48, Th56, TOPS_2:def 1; :: thesis:

end;

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 ) ) } } ;
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 ) ) } } ;
A49: { (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(A20);
A50: { (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;

A51: now

per cases by A4, A7, A38, A43, Th57;

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

then consider a being real number such that
r < a and
a <= s and
A52: 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 A36, A39, A52;
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 A38, XXREAL_1:2; :: thesis:

end;

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

end;

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

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 A49, A50, A51;
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
A53: kL = upper_bound [.r,b.[ and
A54: [.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 ) ) } ;
A55: r < b by A21, A54, XXREAL_1:27;
A56: kL = b by A21, A53, A54, Th5, XXREAL_1:27;
r < kL by A53, A55, Th5;
then A57: lower_bound [.r,kL.[ = r by Th4;
A58: upper_bound [.r,kL.[ = kL by A21, A53, A54, Th5, XXREAL_1:27;
reconsider LEWY = [.r,kL.[ as non empty Subset of (Closed-Interval-TSpace r,s) by A21, A53, A54, Th5, XXREAL_1:27;
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 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 ) ) } } ;
A59: { (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(A20);
A60: { (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;

A61: now

per cases by A4, A7, A40, A45, Th57;

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

hence not { (lower_bound ].c,s.]) where c is Real : ].c,s.] in G \ { X where X is Subset of (Closed-Interval-TSpace r,s) : ( X in G & ex Y being Subset of (Closed-Interval-TSpace r,s) st
( Y in G & X c< Y ) ) } } is empty by A40, 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
A62: 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 A36, A41, A62;
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;

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

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 A59, A60, A61;
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
A63: pP = lower_bound ].b,s.] and
A64: ].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 ) ) } ;
A65: b < s by A21, A64, XXREAL_1:26;
A66: pP = b by A21, A63, A64, Th6, XXREAL_1:26;
A67: s in ].b,s.] by A65, XXREAL_1:2;
pP < s by A63, A65, Th6;
then A68: upper_bound ].pP,s.] = s by Th7;
A69: lower_bound ].pP,s.] = pP by A21, A63, A64, Th6, XXREAL_1:26;
reconsider PRAWY = ].pP,s.] as non empty Subset of (Closed-Interval-TSpace r,s) by A21, A63, A64, Th6, XXREAL_1:26;
A70: 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
A71: r in A and
A72: 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:
assume A73: A <> LEWY ; :: thesis:
A74: A in F by A27, A72;
A75: A is open by A2, A27, A72, TOPS_2:def 1;
A76: A is connected by A3, A27, A72, Def1;

now

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

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

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

end;

then consider ak being real number such that
A78: ( r < ak & ak <= s & A = [.r,ak.[ ) by A4, A7, A71, A74, A75, A76, Th57;
A79: ak is Real by XREAL_0:def 1;
A c= LEWY

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A80: a in A ; :: thesis:
then a in [.r,s.] by A10;
then reconsider a = a as Real ;
A81: r <= a by A78, A80, XXREAL_1:3;
A82: a < ak by A78, A80, XXREAL_1:3;
upper_bound A = ak by A78, Th5;
then ak in LM by A72, A78, A79;
then ak <= kL by XXREAL_2:def 8;
then a < kL by A82, XXREAL_0:2;
hence a in LEWY by A81, XXREAL_1:3; :: thesis:

end;

then A c< LEWY 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 A19, A54, A56, A72;
hence contradiction by A72, XBOOLE_0:def 5; :: thesis:

end;

A83: 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
A84: s in A and
A85: 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:
assume A86: A <> PRAWY ; :: thesis:
A87: A in F by A27, A85;
A88: A is open by A2, A27, A85, TOPS_2:def 1;
A89: A is connected by A3, A27, A85, Def1;

now

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

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

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

end;

then consider ak being real number such that
A91: ( r <= ak & ak < s & A = ].ak,s.] ) by A4, A7, A84, A87, A88, A89, Th57;
A92: ak is Real by XREAL_0:def 1;
A c= PRAWY

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A93: a in A ; :: thesis:
then a in [.r,s.] by A10;
then reconsider a = a as Real ;
A94: a <= s by A91, A93, XXREAL_1:2;
A95: ak < a by A91, A93, XXREAL_1:2;
lower_bound A = ak by A91, Th6;
then ak in RM by A85, A91, A92;
then pP <= ak by XXREAL_2:def 7;
then pP < a by A95, XXREAL_0:2;
hence a in PRAWY by A94, XXREAL_1:2; :: thesis:

end;

then A c< PRAWY by A86, 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 A19, A64, A66, A85;
hence contradiction by A85, XBOOLE_0:def 5; :: thesis:

end;

A96: 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
A97: 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
A98: A <> LEWY and
A99: A <> PRAWY ; :: thesis:
A100: A in F by A27, A97;
A101: ( A is open & A is connected ) by A2, A3, A27, A97, Def1, TOPS_2:def 1;

per cases by A4, A7, A21, A97, A100, A101, Th57;

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

then consider a being real number such that
( r < a & a <= s ) and
A102: A = [.r,a.[ ;

per cases ;

suppose a <= kL ; :: thesis:

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

end;

suppose a > kL ; :: thesis:

then LEWY c= A by A102, XXREAL_1:38;
then LEWY c< A by A98, 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 A19, A54, A56, A97;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A54, A56, 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 & a < s ) and
A103: A = ].a,s.] ;

per cases ;

suppose a >= pP ; :: thesis:

then A c= PRAWY by A103, XXREAL_1:42;
then A c< PRAWY by A99, 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 A19, A64, A66, A97;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A97, XBOOLE_0:def 5; :: thesis:

end;

suppose a < pP ; :: thesis:

then PRAWY c= A by A103, XXREAL_1:42;
then PRAWY c< A by A99, 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 A19, A64, A66, A97;
hence ex a, b being Real st
( a < b & A = ].a,b.[ ) by A64, A66, 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
A104: ( r <= a & a < b & b <= s & 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 A104; :: thesis:

end;

A105: 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
A106: 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
A107: upper_bound A in A and
A108: A <> PRAWY ; :: thesis:
A <> LEWY by A58, A107, XXREAL_1:3;
then consider a, b being Real such that
A109: ( a < b & A = ].a,b.[ ) by A96, A106, A108;
upper_bound A = b by A109, TOPREAL6:22;
hence contradiction by A107, A109, 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 );
A110: 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 ( 1 <= n & n < card X ) ; :: thesis:
let x be Element of X; :: thesis:
reconsider x1 = x as Subset of REAL ;
A111: not x1 is empty by A47;
A112: x c= union X by ZFMISC_1:92;
then x c= [.r,s.] by A4, A37, TOPMETR:25;
then x1 is bounded_above by XXREAL_2:43;
then upper_bound x is Element of (Closed-Interval-TSpace r,s) by A10, A37, A111, A112, Th2;
then consider y being set such that
A113: upper_bound x in y and
A114: y in X by A37, TARSKI:def 4;
reconsider y = y as Element of X by A114;
take y ; :: thesis:
take x ; :: thesis:
thus ( x = x & upper_bound x in y ) by A113; :: thesis:

end;

reconsider LLEWY = LEWY as Element of X by A36, A38, A39, A70;
consider IT being FinSequence of X such that
A115: len IT = card X and
A116: ( IT . 1 = LLEWY or card X = 0 ) and
A117: 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(A110);
A118: 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;
take IT ; :: thesis:
thus rng IT c= F by A46, A118, XBOOLE_1:1; :: thesis:
A119: not IT is empty by A115;
then A120: not rng IT is empty ;
then A121: 1 in dom IT by FINSEQ_3:34;
then A122: IT /. 1 = IT . 1 by PARTFUN1:def 8;
A123: len IT in dom IT by A119, FINSEQ_5:6;
A124: for n being natural number st n in dom IT holds
( IT . n in X & IT /. n in X )

proof

let n be natural number ; :: thesis:
assume A125: n in dom IT ; :: thesis:
A126: IT . n = IT /. n by A125, PARTFUN1:def 8;
IT . n in rng IT by A125, FUNCT_1:def 5;
hence ( IT . n in X & IT /. n in X ) by A118, A126; :: thesis:

end;

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

proof

let n be natural number ; :: thesis:
assume A128: n in dom IT ; :: thesis:
A129: IT . n = IT /. n by A128, PARTFUN1:def 8;
IT . n in X by A124, A128;
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 A36, A129; :: thesis:

end;

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

proof

let i be natural number ; :: thesis:
assume A131: i in dom IT ; :: thesis:
defpred S₃[ natural number ] means ( $1 in dom IT implies for x being Point of (Closed-Interval-TSpace r,s) st x < upper_bound (IT /. $1) holds
ex j being natural number st
( j in dom IT & j <= $1 & x in IT /. j ) );
A132: S₃[ 0 ] by FINSEQ_3:26;
A133: for n being natural number st S₃[n] holds
S₃[n + 1]

proof

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

per cases by A135, TOPREALA:23;

suppose A138: n = 0 ; :: thesis:

take 1 ; :: thesis:
thus 1 in dom IT by A120, FINSEQ_3:34; :: thesis:
thus 1 <= n + 1 by A138; :: thesis:
r <= x by A10, XXREAL_1:1;
hence x in IT /. 1 by A58, A116, A136, A137, A138, XXREAL_1:3; :: thesis:

end;

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

then A140: IT /. n = IT . n by PARTFUN1:def 8;
A141: 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 A127, A135;
A142: IT /. (n + 1) in X by A124, A135;
A143: IT /. (n + 1) is connected Subset of REAL by A28, A141;
A144: not IT /. (n + 1) is empty by A21, A127, A135;
A145: IT /. (n + 1) is bounded_below by A18, A142;
A146: 1 <= n by A139, FINSEQ_3:27;
n + 1 <= len IT by A135, FINSEQ_3:27;
then n < len IT by NAT_1:13;
then A147: ex S being Element of X st
( S = IT . n & upper_bound S in IT . (n + 1) ) by A115, A117, A139, A146;
then A148: lower_bound (IT /. (n + 1)) <= upper_bound (IT /. n) by A137, A140, A145, SEQ_4:def 5;

per cases by XXREAL_0:1;

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

then consider j being natural number such that
A149: j in dom IT and
A150: j <= n and
A151: x in IT /. j by A134, A139;
take j ; :: thesis:
thus j in dom IT by A149; :: thesis:
j + 0 < n + 1 by A150, XREAL_1:10;
hence j <= n + 1 ; :: thesis:
thus x in IT /. j by A151; :: thesis:

end;

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

take n + 1 ; :: thesis:
thus n + 1 in dom IT by A135; :: thesis:
thus n + 1 <= n + 1 ; :: thesis:
thus x in IT /. (n + 1) by A137, A139, A147, A152, PARTFUN1:def 8; :: thesis:

end;

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

take n + 1 ; :: thesis:
thus n + 1 in dom IT by A135; :: thesis:
thus n + 1 <= n + 1 ; :: thesis:
lower_bound (IT /. (n + 1)) < x by A148, A153, XXREAL_0:2;
hence x in IT /. (n + 1) by A136, A143, A144, Th42; :: thesis:

end;

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

end;

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

proof

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

proof

let n be natural number ; :: thesis:
assume that
A158: S₃[n] and
A159: n + 1 in dom IT ; :: thesis:
A160: IT /. (n + 1) = IT . (n + 1) by A159, PARTFUN1:def 8;
assume i < n + 1 ; :: thesis:
then A161: i <= n by NAT_1:13;

per cases by A159, TOPREALA:23;

suppose n = 0 ; :: thesis:

then i = 0 by A161;
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 A155, FINSEQ_3:26; :: thesis:

end;

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

then A163: IT /. n = IT . n by PARTFUN1:def 8;
then A164: IT /. n in rng IT by A162, FUNCT_1:def 5;
A165: IT /. n in X by A124, A162;
then A166: IT /. n is bounded_above by A18;
A167: not IT /. n is empty by A47, A118, A164;
A168: IT /. n is Subset of (Closed-Interval-TSpace r,s) by A47, A118, A164;
A169: n is Element of NAT by ORDINAL1:def 13;
A170: 1 <= n by A162, FINSEQ_3:27;
A171: n + 1 <= len IT by A159, FINSEQ_3:27;
then n < card X by A115, NAT_1:13;
then consider S being Element of X such that
A172: S = IT . n and
A173: upper_bound S in IT . (n + 1) by A117, A169, A170;
A174: IT /. (n + 1) in rng IT by A159, A160, FUNCT_1:def 5;
A175: IT /. (n + 1) in X by A124, A159;
A176: IT /. (n + 1) is open connected Subset of (Closed-Interval-TSpace r,s) by A47, A118, A174;
then A177: IT /. (n + 1) is connected Subset of REAL by Th56;
A178: IT /. (n + 1) is bounded_below by A18, A176;
A179: not IT /. (n + 1) is empty by A47, A118, A174;
A180: IT /. (n + 1) is bounded_above by A18, A176;
then A181: upper_bound S <= upper_bound (IT /. (n + 1)) by A160, A173, SEQ_4:def 4;
A182: lower_bound (IT /. (n + 1)) <= upper_bound S by A160, A173, A178, SEQ_4:def 5;
upper_bound (IT /. (n + 1)) in [.r,s.] by A10, A176, A179, A180, Th2;
then A183: upper_bound (IT /. (n + 1)) <= s by XXREAL_1:1;
upper_bound (IT /. n) in [.r,s.] by A10, A166, A167, A168, Th2;
then A184: upper_bound (IT /. n) <= s by XXREAL_1:1;

per cases by A161, XXREAL_0:1;

suppose i < n ; :: thesis:

then consider y being Point of (Closed-Interval-TSpace r,s) such that
A185: y in IT /. n and
A186: for x being Point of (Closed-Interval-TSpace r,s) st x in IT /. i holds
x < y by A158, A162;
A187: y <= upper_bound (IT /. n) by A166, A185, SEQ_4:def 4;

per cases by A181, XXREAL_0:1;

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

set y1 = ((upper_bound S) + (upper_bound (IT /. (n + 1)))) / 2;
A189: upper_bound S < ((upper_bound S) + (upper_bound (IT /. (n + 1)))) / 2 by A188, XREAL_1:228;
A190: ((upper_bound S) + (upper_bound (IT /. (n + 1)))) / 2 < upper_bound (IT /. (n + 1)) by A188, XREAL_1:228;
then A191: ((upper_bound S) + (upper_bound (IT /. (n + 1)))) / 2 < s by A183, XXREAL_0:2;
upper_bound S in [.r,s.] by A10, A163, A166, A167, A168, A172, Th2;
then r <= upper_bound S by XXREAL_1:1;
then r <= ((upper_bound S) + (upper_bound (IT /. (n + 1)))) / 2 by A189, XXREAL_0:2;
then reconsider y1 = ((upper_bound S) + (upper_bound (IT /. (n + 1)))) / 2 as Point of (Closed-Interval-TSpace r,s) by A10, A191, XXREAL_1:1;
take y1 ; :: thesis:
lower_bound (IT /. (n + 1)) < y1 by A182, A189, XXREAL_0:2;
hence y1 in IT /. (n + 1) by A177, A179, A190, Th42; :: 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 A186, A187, XXREAL_0:2;
hence x < y1 by A163, A172, A189, XXREAL_0:2; :: thesis:

end;

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

then A192: IT /. (n + 1) = PRAWY by A36, A105, A160, A173, A175;
reconsider y1 = s as Point of (Closed-Interval-TSpace r,s) by A4, A10, XXREAL_1:1;
take y1 ; :: thesis:
thus y1 in IT /. (n + 1) by A65, A66, A192, 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 A186, A187, XXREAL_0:2;
hence x < y1 by A184, XXREAL_0:2; :: thesis:

end;

suppose A193: i = n ; :: thesis:

reconsider y1 = upper_bound (IT /. n) as Element of (Closed-Interval-TSpace r,s) by A10, A166, A167, A168, Th2;
take y1 ; :: thesis:
thus y1 in IT /. (n + 1) by A160, A162, A172, A173, PARTFUN1:def 8; :: thesis:
let x be Point of (Closed-Interval-TSpace r,s); :: thesis:
assume A194: x in IT /. i ; :: thesis:
then A195: x <= upper_bound (IT /. n) by A166, A193, SEQ_4:def 4;

now

assume x = upper_bound (IT /. n) ; :: thesis:
then A196: IT /. n = PRAWY by A36, A105, A165, A193, A194;
set IT1 = IT | (Seg n);
A197: rng (IT | (Seg n)) c= rng IT by RELAT_1:99;
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 A197;
then A in X by A118;
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) ;

A198: now

assume A199: FI <> X ; :: thesis:
A200: FI c= X by A118, A197, XBOOLE_1:1;
then A201: FI 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 A36, XBOOLE_1:1;
union FI = the carrier of (Closed-Interval-TSpace r,s)

proof

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

per cases ;

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

then consider j being natural number such that
A202: j in dom IT and
A203: j <= n and
A204: l in IT /. j by A130, A162;
A205: IT . j = IT /. j by A202, PARTFUN1:def 8;
1 <= j by A202, FINSEQ_3:27;
then j in Seg n by A203, FINSEQ_1:3;
then IT . j in FI by A202, FUNCT_1:73;
hence l in union FI by A204, A205, TARSKI:def 4; :: thesis:

end;

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

l <= s by A10, XXREAL_1:1;
then A207: l = s by A68, A196, A206, XXREAL_0:1;
n in Seg n by A170, FINSEQ_1:3;
then IT . n in FI by A162, FUNCT_1:73;
hence l in union FI by A66, A67, A163, A196, A207, TARSKI:def 4; :: thesis:

end;

then FI is Cover of (Closed-Interval-TSpace r,s) by SETFAM_1:def 12;
then A208: FI 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 A201;
then [FI,M] 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 A31, A33, A34, A200, WELLORD2:def 1;
hence contradiction by A31, A32, A34, A199, A208, ORDERS_1:def 12; :: thesis:

end;

A209: card (rng (IT | (Seg n))) <= card (dom (IT | (Seg n))) by CARD_2:66;
Seg n c= dom IT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A210: x in Seg n ; :: thesis:
then reconsider x = x as Nat ;
A211: 1 <= x by A210, FINSEQ_1:3;
A212: x <= n by A210, FINSEQ_1:3;
n + 0 <= n + 1 by XREAL_1:8;
then x <= n + 1 by A212, XXREAL_0:2;
then x <= len IT by A171, XXREAL_0:2;
hence x in dom IT by A211, FINSEQ_3:27; :: thesis:

end;

then dom (IT | (Seg n)) = Seg n by RELAT_1:91;
then card (dom (IT | (Seg n))) = n by FINSEQ_1:78;
then n + 1 <= n + 0 by A115, A171, A198, A209, XXREAL_0:2;
hence contradiction by XREAL_1:8; :: thesis:

end;

hence x < y1 by A195, XXREAL_0:1; :: thesis:

end;

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

end;

A213: IT is Function of (dom IT),X by A118, FUNCT_2:4;
dom IT = Seg (len IT) by FINSEQ_1:def 3;
then A214: card (dom IT) = card X by A115, FINSEQ_1:78;
A215: IT is one-to-one

proof

let i, j be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A216: i in dom IT and
A217: j in dom IT and
A218: IT . i = IT . j ; :: thesis:
assume A219: i <> j ; :: thesis:
A220: ( IT /. i = IT . i & IT /. j = IT . j ) by A216, A217, PARTFUN1:def 8;
reconsider i = i, j = j as Nat by A216, A217;

per cases by A219, 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 A154, A216, A217;
hence contradiction by A218, A220; :: 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 A154, A216, A217;
hence contradiction by A218, A220; :: thesis:

end;

then A221: rng IT = X by A213, A214, FINSEQ_4:78;
hence union (rng IT) = [.r,s.] by A4, A37, TOPMETR:25; :: thesis:
A222: for i, j being natural number st i in dom IT & j in dom IT & i <> j holds
IT /. i <> IT /. j

proof

let i, j be natural number ; :: thesis:
assume that
A223: i in dom IT and
A224: j in dom IT and
A225: i <> j ; :: thesis:
( IT /. i = IT . i & IT /. j = IT . j ) by A223, A224, PARTFUN1:def 8;
hence IT /. i <> IT /. j by A215, A223, A224, A225, FUNCT_1:def 8; :: thesis:

end;

ex Z being set st
( s in Z & Z in C ) by A9, A10, A37, TARSKI:def 4;
then PRAWY in X by A36, A83;
then consider i being set such that
A226: i in dom IT and
A227: IT . i = PRAWY by A221, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A226;
A228: 1 <= i by A226, FINSEQ_3:27;
A229: i <= len IT by A226, FINSEQ_3:27;
A230: IT /. i = IT . i by A226, PARTFUN1:def 8;

A231: now

assume i <> len IT ; :: thesis:
then A232: i < len IT by A229, XXREAL_0:1;
then A233: ex S being Element of X st
( S = IT . i & upper_bound S in IT . (i + 1) ) by A115, A117, A228;
A234: 0 + 1 <= i + 1 by XREAL_1:8;
i + 1 <= len IT by A232, NAT_1:13;
then A235: i + 1 in dom IT by A234, FINSEQ_3:27;
then A236: IT /. (i + 1) = IT . (i + 1) by PARTFUN1:def 8;
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 A127, A235;
then i + 0 = i + 1 by A68, A83, A222, A226, A227, A230, A233, A235, A236;
hence contradiction ; :: thesis:

end;

A237: for n being natural number st 1 < n & n < len IT holds
ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ )

proof

let n be natural number ; :: thesis:
assume that
A238: 1 < n and
A239: n < len IT ; :: thesis:
A240: n in dom IT by A238, A239, FINSEQ_3:27;
then IT . n in rng IT by FUNCT_1:def 5;
then A241: IT /. n in rng IT by A240, PARTFUN1:def 8;
then A242: IT /. n in X by A118;
then A243: 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 A36;
A244: IT /. n in F by A46, A242;
A245: IT /. n is open connected Subset of (Closed-Interval-TSpace r,s) by A47, A118, A241;

per cases by A4, A7, A21, A243, A244, A245, Th57;

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

then consider a being real number such that
A246: r < a and
a <= s and
A247: IT /. n = [.r,a.[ ;
r in [.r,a.[ by A246, XXREAL_1:3;
then IT /. n = LEWY by A36, A70, A242, A247;
hence ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A116, A121, A122, A222, A238, A240; :: 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
A248: a < s and
A249: IT /. n = ].a,s.] ;
A250: upper_bound ].a,s.] = s by A248, Th7;
s in ].a,s.] by A248, XXREAL_1:2;
then IT /. n = PRAWY by A36, A105, A242, A249, A250;
hence ex a, b being Real st
( r <= a & a < b & b <= s & IT /. n = ].a,b.[ ) by A123, A222, A227, A230, A231, A239, A240; :: 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
A251: ( 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 A251; :: thesis:

end;

A252: now

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

hereby :: thesis:

assume A254: n <= len IT ; :: thesis:
then A255: m in dom IT by A253, FINSEQ_3:27;
IT /. n = IT . n by A253, A254, FINSEQ_4:24;
then IT /. n in rng IT by A255, FUNCT_1:def 5;
then IT /. n in X by A118;
hence not IT /. n is empty by A21, A36; :: thesis:

end;

hereby :: thesis:

assume A256: n + 1 <= len IT ; :: thesis:
then A257: m < len IT by NAT_1:13;
then A258: ex S being Element of X st
( S = IT . n & upper_bound S in IT . (n + 1) ) by A115, A117, A253;
A259: IT /. n = IT . n by A253, A257, FINSEQ_4:24;
A260: 1 < m + 1 by A253, NAT_1:13;
then A261: IT /. (m + 1) = IT . (m + 1) by A256, FINSEQ_4:24;
A262: m in dom IT by A253, A257, FINSEQ_3:27;
then IT /. n in rng IT by A259, FUNCT_1:def 5;
then A263: IT /. n in X by A118;
then A264: 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 A36;
A265: n + 1 in dom IT by A256, A260, FINSEQ_3:27;
then A266: IT /. (n + 1) in rng IT by A261, FUNCT_1:def 5;
then A267: IT /. (n + 1) in X by A118;
then A268: 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 A36;
n + 0 < n + 1 by XREAL_1:8;
then A269: IT /. n <> IT /. (n + 1) by A222, A262, A265;
A270: IT /. n is non empty bounded connected Subset of REAL by A18, A21, A28, A36, A263;
A271: IT /. (n + 1) is non empty bounded connected Subset of REAL by A18, A21, A28, A36, A267;
IT /. (n + 1) c= union X by A118, A266, ZFMISC_1:92;
then IT /. (n + 1) c= [.r,s.] by A4, A37, TOPMETR:25;
then A272: IT /. (n + 1) is bounded_above by XXREAL_2:43;
then A273: upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) by A258, A259, A261, SEQ_4:def 4;

hereby :: thesis:

assume A274: 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 A36, A105, A123, A222, A227, A230, A231, A257, A262, A263;
then IT /. n c= IT /. (n + 1) by A270, A271, A273, A274, Th43;
then IT /. n c< IT /. (n + 1) by A269, 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 A19, A264, A268;
hence contradiction by A36, A263, XBOOLE_0:def 5; :: thesis:

end;

thus upper_bound (IT /. n) <= upper_bound (IT /. (n + 1)) by A258, A259, A261, A272, SEQ_4:def 4; :: thesis:

per cases by A256, XXREAL_0:1;

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

then pP < upper_bound (IT /. n) by A227, A231, A258, A259, XXREAL_1:2;
hence lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) by A227, A230, A231, A275, Th6, XXREAL_1:26; :: thesis:

end;

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

then consider a1, b1 being Real such that
r <= a1 and
A276: a1 < b1 and
b1 <= s and
A277: IT /. (n + 1) = ].a1,b1.[ by A237, A260;
a1 < upper_bound (IT /. n) by A258, A259, A261, A277, XXREAL_1:4;
hence lower_bound (IT /. (n + 1)) < upper_bound (IT /. n) by A276, A277, TOPREAL6:22; :: thesis:

end;

hereby :: thesis:

let n be natural number ; :: thesis:
assume A278: 1 <= n ; :: thesis:
thus A279: ( ( 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 A252, A278; :: thesis:
assume A280: n + 2 <= len IT ; :: thesis:
assume A281: upper_bound (IT /. n) > lower_bound (IT /. (n + 2)) ; :: thesis:
reconsider m = n as Nat ;
0 + 1 <= n + 1 by XREAL_1:8;
then A282: upper_bound (IT /. (n + 1)) <= upper_bound (IT /. ((n + 1) + 1)) by A252, A280;
A283: n + 0 < n + 1 by XREAL_1:8;
then A284: 1 < m + 1 by A278, XXREAL_0:2;
A285: (n + 1) + 1 <= len IT by A280;
then A286: m + 1 < len IT by NAT_1:13;
then consider a1, b1 being Real such that
r <= a1 and
A287: a1 < b1 and
b1 <= s and
A288: IT /. (n + 1) = ].a1,b1.[ by A237, A284;
A289: upper_bound ].a1,b1.[ = b1 by A287, TOPREAL6:22;
A290: lower_bound ].a1,b1.[ = a1 by A287, TOPREAL6:22;
m <= len IT by A283, A286, XXREAL_0:2;
then A291: n in dom IT by A278, FINSEQ_3:27;
then IT /. n = IT . n by PARTFUN1:def 8;
then IT /. n in rng IT by A291, FUNCT_1:def 5;
then A292: IT /. n in X by A118;
A293: n + 1 in dom IT by A284, A286, FINSEQ_3:27;
then IT /. (n + 1) = IT . (n + 1) by PARTFUN1:def 8;
then IT /. (n + 1) in rng IT by A293, FUNCT_1:def 5;
then A294: IT /. (n + 1) in X by A118;
m + 1 <= m + 2 by XREAL_1:8;
then 1 <= m + 2 by A284, XXREAL_0:2;
then A295: m + 2 in dom IT by A280, FINSEQ_3:27;
then IT /. (n + 2) = IT . (n + 2) by PARTFUN1:def 8;
then IT /. (n + 2) in rng IT by A295, FUNCT_1:def 5;
then A296: IT /. (n + 2) in X by A118;
n + 0 < n + 1 by XREAL_1:8;
then A297: IT /. n <> IT /. (n + 1) by A222, A291, A293;
n + 1 < n + 2 by XREAL_1:8;
then A298: IT /. (n + 2) <> IT /. (n + 1) by A222, A293, A295;
IT /. (n + 1) c= (IT /. n) \/ (IT /. (n + 2))

proof

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

per cases ;

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

per cases ;

suppose A302: n = 1 ; :: thesis:

then lower_bound (IT /. n) <= x by A10, A57, A116, A122, A294, A299, XXREAL_1:1;
then x in IT /. n by A53, A56, A57, A116, A122, A301, A302, XXREAL_1:3;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

suppose n <> 1 ; :: thesis:

then A303: 1 < n by A278, XXREAL_0:1;
n + 0 < n + 2 by XREAL_1:8;
then n < len IT by A280, XXREAL_0:2;
then consider a, b being Real such that
r <= a and
A304: a < b and
b <= s and
A305: IT /. n = ].a,b.[ by A237, A303;
A306: lower_bound (IT /. n) = a by A304, A305, TOPREAL6:22;
A307: upper_bound (IT /. n) = b by A304, A305, TOPREAL6:22;
lower_bound (IT /. n) < x by A279, A285, A288, A290, A300, NAT_1:13, XXREAL_0:2;
then x in IT /. n by A301, A305, A306, A307, 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 A308: x > lower_bound (IT /. (n + 2)) by A281, XXREAL_0:2;

per cases ;

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

x <= s by A10, A294, A299, XXREAL_1:1;
then x in IT /. (n + 2) by A69, A227, A230, A231, A308, A309, XXREAL_1:2;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

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

then A310: (n + 1) + 1 < len IT by A280, XXREAL_0:1;
n + 1 < n + 2 by XREAL_1:8;
then 1 < n + 2 by A284, XXREAL_0:2;
then consider a2, b2 being Real such that
r <= a2 and
A311: a2 < b2 and
b2 <= s and
A312: IT /. (n + 2) = ].a2,b2.[ by A237, A310;
A313: upper_bound ].a2,b2.[ = b2 by A311, TOPREAL6:22;
A314: lower_bound ].a2,b2.[ = a2 by A311, TOPREAL6:22;
x < b2 by A282, A288, A289, A300, A312, A313, XXREAL_0:2;
then x in IT /. (n + 2) by A308, A312, A314, XXREAL_1:4;
hence x in (IT /. n) \/ (IT /. (n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

hence contradiction by A32, A33, A34, A292, A294, A296, A297, A298, Th62; :: thesis:

end;

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

proof

take kL ; :: thesis:
thus r < kL by A53, A55, Th5; :: thesis:
upper_bound LEWY <= upper_bound [.r,s.] by A10, SEQ_4:65;
hence kL <= s by A4, A58, JORDAN5A:20; :: thesis:
thus IT . 1 = [.r,kL.[ by A116; :: 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 A10, SEQ_4:64;
hence r <= pP by A4, A69, JORDAN5A:20; :: thesis:
thus pP < s by A63, A65, Th6; :: thesis:
thus IT . (len IT) = ].pP,s.] by A227, A231; :: thesis:

end;

let n be natural number ; :: thesis:
assume A315: ( 1 < n & n < len IT ) ; :: thesis:
consider a, b being Real such that
A316: r <= a and
A317: a < b and
A318: b <= s and
A319: IT /. n = ].a,b.[ by A237, A315;
take a ; :: thesis:
take b ; :: thesis:
thus ( r <= a & a < b & b <= s & IT . n = ].a,b.[ ) by A315, A316, A317, A318, A319, FINSEQ_4:24; :: thesis:

end;