:: deftheorem Def3 defines Closed-Interval-MSpace TOPMETR:def 3 :
for a, b being Real st a <= b holds
for b₃ being non empty strict SubSpace of RealSpace holds
( b₃ = Closed-Interval-MSpace (a,b) iff for P being non empty Subset of RealSpace st P = [.a,b.] holds
b₃ = RealSpace | P );