reconsider MM = MetrStruct(# the carrier of M, the distance of M #) as MetrSpace by Lm1;
for x, y being Point of MM holds the distance of MM . (x,y) = the distance of M . (x,y) ;
then MM is SubSpace of M by Def1;
hence ex b₁ being SubSpace of M st
( b₁ is strict & not b₁ is empty ) ; :: thesis: verum