let r, s be Real; :: 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 st
( r < a & a <= s & X = [.r,a.[ ) or ex a being Real st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being Real 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 st
( r < a & a <= s & X = [.r,a.[ ) or ex a being Real st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being Real st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )
then A2: the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] by TOPMETR:18;
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 st
( r < a & a <= s & X = [.r,a.[ ) or ex a being Real st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being Real st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )
X is bounded_below bounded_above Subset of REAL by A2, XBOOLE_1:1, XXREAL_2:43, XXREAL_2:44;
then reconsider Y = X as real-bounded interval Subset of REAL by Th43;
A3: ( the carrier of (Closed-Interval-TSpace (r,s)) = [#] (Closed-Interval-TSpace (r,s)) & Closed-Interval-TSpace (r,s) is connected ) by A1, TREAL_1:20;
A4: s in [.r,s.] by A1, XXREAL_1:1;
A5: r in [.r,s.] by A1, XXREAL_1:1;

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

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

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

end;

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

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

end;

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

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

now :: thesis: ( not r <> a & not b <> s )

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

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

suppose r < a ; :: thesis: contradiction

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

end;

suppose b < s ; :: thesis: contradiction

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

end;

end;

end;

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

end;

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

then consider a, b being Real such that
A12: a < b and
A13: Y = [.a,b.[ ;
A14: b <= s by A2, A12, A13, XXREAL_1:52;
A15: r <= a by A2, A12, A13, XXREAL_1:52;

now :: thesis: not r <> a

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

now :: thesis: not Int X = X

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

end;

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

end;

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

end;

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

then consider a, b being Real such that
A18: a < b and
A19: Y = ].a,b.] ;
A20: r <= a by A2, A18, A19, XXREAL_1:53;
A21: b <= s by A2, A18, A19, XXREAL_1:53;

now :: thesis: not b <> s

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

now :: thesis: not Int X = X

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

end;

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

end;

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

end;

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

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

end;

end;