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_{1} being SubSpace of M st b_{1} is strict
; :: thesis: verum

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