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

hence TopSpaceMetr M = TopSpaceMetr N by A1, A4, PCOMPS_1:def 5; :: thesis: verum

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

TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #)
by PCOMPS_1:def 5;
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

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 )

end;proof

let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in Family_open_set N or X in Family_open_set M )
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 )

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

hence
X in Family_open_set N
by A1, A5, PCOMPS_1:def 4; :: thesis: verum
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;( 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

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

hence
X in Family_open_set M
by A1, A10, PCOMPS_1:def 4; :: thesis: verum
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;( 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

hence TopSpaceMetr M = TopSpaceMetr N by A1, A4, PCOMPS_1:def 5; :: thesis: verum