let M, N be non empty MetrSpace; :: thesis: ( the carrier of M = the carrier of N & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) ) & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ) implies TopSpaceMetr M = TopSpaceMetr N )
assume that
A1: the carrier of M = the carrier of N and
A2: for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) and
A3: for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ; :: thesis: TopSpaceMetr M = TopSpaceMetr N
A4: Family_open_set M = Family_open_set N

proof

thus Family_open_set M c= Family_open_set N :: according to XBOOLE_0:def 10 :: thesis: Family_open_set N c= Family_open_set M

proof

let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in Family_open_set M or X in Family_open_set N )
reconsider XX = X as set by TARSKI:1;
assume A5: X in Family_open_set M ; :: thesis: X in Family_open_set N
for n being Point of N st n in XX holds
ex r being Real st
( r > 0 & Ball (n,r) c= XX )

proof

let n be Point of N; :: thesis: ( n in XX implies ex r being Real st
( r > 0 & Ball (n,r) c= XX ) )
assume A6: n in XX ; :: thesis: ex r being Real st
( r > 0 & Ball (n,r) c= XX )
reconsider m = n as Point of M by A1;
consider r being Real such that
A7: r > 0 and
A8: Ball (m,r) c= XX by A5, A6, PCOMPS_1:def 4;
consider r1 being Real such that
A9: ( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) by A2, A7;
take r1 ; :: thesis: ( r1 > 0 & Ball (n,r1) c= XX )
thus ( r1 > 0 & Ball (n,r1) c= XX ) by A8, A9; :: thesis: verum

end;

hence X in Family_open_set N by A1, A5, PCOMPS_1:def 4; :: thesis: verum

end;

let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in Family_open_set N or X in Family_open_set M )
reconsider XX = X as set by TARSKI:1;
assume A10: X in Family_open_set N ; :: thesis: X in Family_open_set M
for m being Point of M st m in XX holds
ex r being Real st
( r > 0 & Ball (m,r) c= XX )

proof

let m be Point of M; :: thesis: ( m in XX implies ex r being Real st
( r > 0 & Ball (m,r) c= XX ) )
assume A11: m in XX ; :: thesis: ex r being Real st
( r > 0 & Ball (m,r) c= XX )
reconsider n = m as Point of N by A1;
consider r being Real such that
A12: r > 0 and
A13: Ball (n,r) c= XX by A10, A11, PCOMPS_1:def 4;
consider r1 being Real such that
A14: ( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) by A3, A12;
take r1 ; :: thesis: ( r1 > 0 & Ball (m,r1) c= XX )
thus ( r1 > 0 & Ball (m,r1) c= XX ) by A13, A14; :: thesis: verum

end;

hence X in Family_open_set M by A1, A10, PCOMPS_1:def 4; :: thesis: verum

end;

TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;
hence TopSpaceMetr M = TopSpaceMetr N by A1, A4, PCOMPS_1:def 5; :: thesis: verum