theorem :: TOPREALA:26

for a, b, r being Real st a <= b & r <= b holds
[.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b))