let a, b, r be Real; :: 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:18;
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: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: x < r by A6, XXREAL_1:4;
a <= x by A3, A5, XXREAL_1:1;
hence x in A by A7; :: thesis: verum
end;
a - 1 < a - 0 by XREAL_1:15;
then A c= C by XXREAL_1:48;
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 [.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; :: thesis: verum