reconsider B = A as non empty set ;
set d = the distance of M || A;
A1: dom (the distance of M || A) = (dom the distance of M) /\ [:A,A:] by RELAT_1:90
.= [:the carrier of M,the carrier of M:] /\ [:A,A:] by FUNCT_2:def 1
.= [:(the carrier of M /\ A),(the carrier of M /\ A):] by ZFMISC_1:123
.= [:(the carrier of M /\ A),A:] by XBOOLE_1:28
.= [:A,A:] by XBOOLE_1:28 ;
the distance of M || A = the distance of M | [:A,A:] ;
then rng (the distance of M || A) c= REAL by RELAT_1:def 19;
then reconsider d = the distance of M || A as Function of [:B,B:],REAL by A1, FUNCT_2:def 1, RELSET_1:11;
set MM = MetrStruct(# B,d #);

A2: now

let a, b be Element of MetrStruct(# B,d #); :: thesis: dist a,b = the distance of M . a,b
thus dist a,b = the distance of MetrStruct(# B,d #) . a,b
.= the distance of M . [a,b] by A1, FUNCT_1:70
.= the distance of M . a,b ; :: thesis: verum

end;

now

let a, b, c be Element of MetrStruct(# B,d #); :: thesis: ( ( dist a,b = 0 implies a = b ) & ( a = b implies dist a,b = 0 ) & dist a,b = dist b,a & dist a,c <= (dist a,b) + (dist b,c) )
reconsider a9 = a, b9 = b, c9 = c as Point of M by TARSKI:def 3;
A3: dist a,c = the distance of M . a,c by A2
.= dist a9,c9 ;
dist a,b = the distance of M . a,b by A2
.= dist a9,b9 ;
hence ( dist a,b = 0 iff a = b ) by METRIC_1:1, METRIC_1:2; :: thesis: ( dist a,b = dist b,a & dist a,c <= (dist a,b) + (dist b,c) )
A4: dist b,c = the distance of M . b,c by A2
.= dist b9,c9 ;
thus dist a,b = the distance of M . a9,b9 by A2
.= dist b9,a9 by METRIC_1:def 1
.= the distance of M . b9,a9
.= dist b,a by A2 ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)
dist a,b = the distance of M . a,b by A2
.= dist a9,b9 ;
hence dist a,c <= (dist a,b) + (dist b,c) by A3, A4, METRIC_1:4; :: thesis: verum

end;

then reconsider MM = MetrStruct(# B,d #) as MetrSpace by METRIC_1:6;

now

let x, y be Point of MM; :: thesis: the distance of MM . x,y = the distance of M . x,y
thus the distance of MM . x,y = dist x,y
.= the distance of M . x,y by A2 ; :: thesis: verum

end;

then reconsider MM = MM as strict SubSpace of M by Def1;
take MM ; :: thesis: the carrier of MM = A
thus the carrier of MM = A ; :: thesis: verum