let a, r, s, b be real number ; :: thesis: ( a <= r & s <= b implies ].r,s.[ is open Subset of (Closed-Interval-TSpace a,b) )
set T = Closed-Interval-TSpace a,b;
set A = ].r,s.[;
assume that
A1: a <= r and
A2: s <= b ; :: thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace a,b)

per cases ( r >= s or r < s ) ;

suppose r >= s ; :: thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace a,b)

then ].r,s.[ = {} (Closed-Interval-TSpace a,b) by XXREAL_1:28;
hence ].r,s.[ is open Subset of (Closed-Interval-TSpace a,b) ; :: thesis: verum

end;

suppose r < s ; :: thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace a,b)

then a < s by A1, XXREAL_0:2;
then the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] by A2, TOPMETR:25, XXREAL_0:2;
then reconsider A = ].r,s.[ as Subset of (Closed-Interval-TSpace a,b) by A1, A2, XXREAL_1:37;
reconsider C = A as Subset of R^1 by TOPMETR:24;
( C is open & C /\ ([#] (Closed-Interval-TSpace a,b)) = A ) by JORDAN6:46, XBOOLE_1:28;
hence ].r,s.[ is open Subset of (Closed-Interval-TSpace a,b) by TOPS_2:32; :: thesis: verum

end;

end;