:: deftheorem Def1 defines SubSpace TOPMETR:def 1 :
for M, b₂ being MetrSpace holds
( b₂ is SubSpace of M iff ( the carrier of b₂ c= the carrier of M & ( for x, y being Point of b₂ holds the distance of b₂ . (x,y) = the distance of M . (x,y) ) ) );