let a, b, r be real number ; :: thesis: ( a <= b & r <= b implies [.a,r.[ is open Subset of (Closed-Interval-TSpace a,b) )
set T = Closed-Interval-TSpace a,b;
assume that
A1: a <= b and
A2: r <= b ; :: thesis: [.a,r.[ 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 = [.a,r.[ as Subset of (Closed-Interval-TSpace a,b) by A2, XXREAL_1:35;
reconsider C = ].(a - 1),r.[ as Subset of R^1 by TOPMETR:24;
A4: C is open by JORDAN6:46;
C /\ ([#] (Closed-Interval-TSpace a,b)) = A

proof

thus C /\ ([#] (Closed-Interval-TSpace a,b)) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= C /\ ([#] (Closed-Interval-TSpace a,b))

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: a <= x by A3, A5, XXREAL_1:1;
x < r by A6, XXREAL_1:4;
hence x in A by A7; :: thesis: verum

end;

a - 1 < a - 0 by XREAL_1:17;
then A c= C by XXREAL_1:48;
hence A c= C /\ ([#] (Closed-Interval-TSpace a,b)) by XBOOLE_1:19; :: thesis: verum

end;

hence [.a,r.[ is open Subset of (Closed-Interval-TSpace a,b) by A4, TOPS_2:32; :: thesis: verum