let a, b, r be real number ; :: thesis: ( a <= b & a <= r implies ].r,b.] is open Subset of (Closed-Interval-TSpace a,b) )
set T = Closed-Interval-TSpace a,b;
assume that
A1: a <= b and
A2: a <= r ; :: thesis: ].r,b.] is open Subset of (Closed-Interval-TSpace a,b)
A3: the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] by A1, TOPMETR:25;
then reconsider A = ].r,b.] as Subset of (Closed-Interval-TSpace a,b) by A2, XXREAL_1:36;
reconsider C = ].r,(b + 1).[ as Subset of R^1 by TOPMETR:24;
A4: C /\ ([#] (Closed-Interval-TSpace a,b)) c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C /\ ([#] (Closed-Interval-TSpace a,b)) or x in A )
assume A5: x in C /\ ([#] (Closed-Interval-TSpace a,b)) ; :: thesis: x in A
then A6: x in C by XBOOLE_0:def 4;
then reconsider x = x as Real ;
A7: r < x by A6, XXREAL_1:4;
x <= b by A3, A5, XXREAL_1:1;
hence x in A by A7; :: thesis: verum

end;

b + 0 < b + 1 by XREAL_1:8;
then A c= C by XXREAL_1:49;
then A c= C /\ ([#] (Closed-Interval-TSpace a,b)) by XBOOLE_1:19;
then ( C is open & C /\ ([#] (Closed-Interval-TSpace a,b)) = A ) by A4, JORDAN6:46, XBOOLE_0:def 10;
hence ].r,b.] is open Subset of (Closed-Interval-TSpace a,b) by TOPS_2:32; :: thesis: verum