let a, b, r be Real; :: 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:18;
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:17;
A4: C /\ ([#] (Closed-Interval-TSpace (a,b))) c= A

proof

let x be object ; :: 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:6;
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:35;
hence ].r,b.] is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; :: thesis: verum