theorem :: TOPREALA:25

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