let r, s be real number ; :: thesis: ( r <= s implies for X being open connected Subset of (Closed-Interval-TSpace r,s) holds
( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) ) )
set L = Closed-Interval-TSpace r,s;
assume A1: r <= s ; :: thesis: for X being open connected Subset of (Closed-Interval-TSpace r,s) holds
( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )
let X be open connected Subset of (Closed-Interval-TSpace r,s); :: thesis: ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )
A2: the carrier of (Closed-Interval-TSpace r,s) = [#] (Closed-Interval-TSpace r,s) ;
A3: the carrier of (Closed-Interval-TSpace r,s) = [.r,s.] by A1, TOPMETR:25;
then X is bounded_below bounded_above Subset of REAL by XBOOLE_1:1, XXREAL_2:43, XXREAL_2:44;
then reconsider Y = X as bounded connected Subset of REAL by Th56;
A4: Closed-Interval-TSpace r,s is connected by A1, TREAL_1:23;
A5: r in [.r,s.] by A1, XXREAL_1:1;
A6: s in [.r,s.] by A1, XXREAL_1:1;

per cases ( Y is empty or Y = [#] REAL or ex a being real number st Y = left_closed_halfline a or ex a being real number st Y = left_open_halfline a or ex a being real number st Y = right_closed_halfline a or ex a being real number st Y = right_open_halfline a or ex a, b being real number st
( a <= b & Y = [.a,b.] ) or ex a, b being real number st
( a < b & Y = [.a,b.[ ) or ex a, b being real number st
( a < b & Y = ].a,b.] ) or ex a, b being real number st
( a < b & Y = ].a,b.[ ) ) by Th41;

suppose ( Y is empty or Y = [#] REAL ) ; :: thesis: ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )

hence ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) ) ; :: thesis: verum

end;

suppose ( ex a being real number st Y = left_closed_halfline a or ex a being real number st Y = left_open_halfline a or ex a being real number st Y = right_closed_halfline a or ex a being real number st Y = right_open_halfline a ) ; :: thesis: ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )

hence ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) ) ; :: thesis: verum

end;

suppose ex a, b being real number st
( a <= b & Y = [.a,b.] ) ; :: thesis: ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )

then consider a, b being real number such that
A7: a <= b and
A8: Y = [.a,b.] ;
A9: ( r <= a & b <= s ) by A3, A7, A8, XXREAL_1:50;
A10: X <> {} (Closed-Interval-TSpace r,s) by A7, A8, XXREAL_1:1;
A11: X is closed by A8, A9, TOPREALA:44;

now

assume A12: ( r <> a or b <> s ) ; :: thesis: contradiction

per cases ( r < a or b < s ) by A9, A12, XXREAL_0:1;

suppose r < a ; :: thesis: contradiction

then not r in X by A8, XXREAL_1:1;
hence contradiction by A2, A3, A4, A5, A10, A11, CONNSP_1:14; :: thesis: verum

end;

suppose b < s ; :: thesis: contradiction

then not s in X by A8, XXREAL_1:1;
hence contradiction by A2, A3, A4, A6, A10, A11, CONNSP_1:14; :: thesis: verum

end;

end;

end;

hence ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) ) by A8; :: thesis: verum

end;

suppose ex a, b being real number st
( a < b & Y = [.a,b.[ ) ; :: thesis: ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )

then consider a, b being real number such that
A13: a < b and
A14: Y = [.a,b.[ ;
A15: ( r <= a & b <= s ) by A3, A13, A14, XXREAL_1:52;

now

assume r <> a ; :: thesis: contradiction
then A16: r < a by A15, XXREAL_0:1;

now

assume A17: Int X = X ; :: thesis: contradiction
Int X = ].a,b.[ by A1, A14, A15, A16, Th54;
then not a in Int X by XXREAL_1:4;
hence contradiction by A13, A14, A17, XXREAL_1:3; :: thesis: verum

end;

hence contradiction by TOPS_1:55; :: thesis: verum

end;

hence ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) ) by A13, A14, A15; :: thesis: verum

end;

suppose ex a, b being real number st
( a < b & Y = ].a,b.] ) ; :: thesis: ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )

then consider a, b being real number such that
A18: a < b and
A19: Y = ].a,b.] ;
A20: ( r <= a & b <= s ) by A3, A18, A19, XXREAL_1:53;

now

assume b <> s ; :: thesis: contradiction
then A21: b < s by A20, XXREAL_0:1;

now

assume A22: Int X = X ; :: thesis: contradiction
Int X = ].a,b.[ by A1, A19, A20, A21, Th55;
then not b in Int X by XXREAL_1:4;
hence contradiction by A18, A19, A22, XXREAL_1:2; :: thesis: verum

end;

hence contradiction by TOPS_1:55; :: thesis: verum

end;

hence ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) ) by A18, A19, A20; :: thesis: verum

end;

suppose ex a, b being real number st
( a < b & Y = ].a,b.[ ) ; :: thesis: ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )

then consider a, b being real number such that
A23: a < b and
A24: Y = ].a,b.[ ;
( r <= a & b <= s ) by A3, A23, A24, XXREAL_1:51;
hence ( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) ) by A23, A24; :: thesis: verum

end;

end;