let a, b, r, s be Real; :: 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:18, 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:17;
( C is open & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by JORDAN6:35, XBOOLE_1:28;
hence ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; :: thesis: verum
end;
end;