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:61

.= [: 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:100

.= [:( 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:4;

set MM = MetrStruct(# B,d #);

take MM ; :: thesis: the carrier of MM = A

thus the carrier of MM = A ; :: thesis: verum

set d = the distance of M || A;

A1: dom ( the distance of M || A) = (dom the distance of M) /\ [:A,A:] by RELAT_1:61

.= [: 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:100

.= [:( 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:4;

set MM = MetrStruct(# B,d #);

A2: now :: thesis: for a, b being Element of MetrStruct(# B,d #) holds dist (a,b) = the distance of M . (a,b)

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:47

.= the distance of M . (a,b) ; :: thesis: verum

end;thus dist (a,b) = the distance of MetrStruct(# B,d #) . (a,b)

.= the distance of M . [a,b] by A1, FUNCT_1:47

.= the distance of M . (a,b) ; :: thesis: verum

now :: thesis: for a, b, c being Element of MetrStruct(# B,d #) holds

( ( 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)) )

then reconsider MM = MetrStruct(# B,d #) as MetrSpace by METRIC_1:6;( ( 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)) )

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;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

now :: thesis: for x, y being Point of MM holds the distance of MM . (x,y) = the distance of M . (x,y)

then reconsider MM = MM as strict SubSpace of M by Def1;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;thus the distance of MM . (x,y) = dist (x,y)

.= the distance of M . (x,y) by A2 ; :: thesis: verum

take MM ; :: thesis: the carrier of MM = A

thus the carrier of MM = A ; :: thesis: verum