:: deftheorem Def2 defines | TOPMETR:def 2 :
for M being non empty MetrSpace
for A being non empty Subset of M
for b₃ being strict SubSpace of M holds
( b₃ = M | A iff the carrier of b₃ = A );