theorem Th23: :: TOPMETR:23
for a, b, d, e being Real
for B being Subset of (Closed-Interval-TSpace (d,e)) st d <= a & a <= b & b <= e & B = [.a,b.] holds
Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B