for r, s being Real st r <= s holds
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.[ ) )