let M be non empty MetrSpace; :: thesis: for A being non empty SubSpace of M holds TopSpaceMetr A is SubSpace of TopSpaceMetr M
let A be non empty SubSpace of M; :: thesis:
set T = TopSpaceMetr M;
set R = TopSpaceMetr A;
thus [#] () c= [#] () by Def1; :: according to PRE_TOPC:def 4 :: thesis: for b1 being Element of bool the carrier of () holds
( ( not b1 in the topology of () or ex b2 being Element of bool the carrier of () st
( b2 in the topology of () & b1 = b2 /\ ([#] ()) ) ) & ( for b2 being Element of bool the carrier of () holds
( not b2 in the topology of () or not b1 = b2 /\ ([#] ()) ) or b1 in the topology of () ) )

let P be Subset of (); :: thesis: ( ( not P in the topology of () or ex b1 being Element of bool the carrier of () st
( b1 in the topology of () & P = b1 /\ ([#] ()) ) ) & ( for b1 being Element of bool the carrier of () holds
( not b1 in the topology of () or not P = b1 /\ ([#] ()) ) or P in the topology of () ) )

thus ( P in the topology of () implies ex Q being Subset of () st
( Q in the topology of () & P = Q /\ ([#] ()) ) ) :: thesis: ( for b1 being Element of bool the carrier of () holds
( not b1 in the topology of () or not P = b1 /\ ([#] ()) ) or P in the topology of () )
proof
set QQ = { (Ball (x,r)) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) } ;
for X being set st X in { (Ball (x,r)) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) } holds
X c= the carrier of M
proof
let X be set ; :: thesis: ( X in { (Ball (x,r)) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) } implies X c= the carrier of M )
assume X in { (Ball (x,r)) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) } ; :: thesis: X c= the carrier of M
then ex x being Point of M ex r being Real st
( X = Ball (x,r) & x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) ;
hence X c= the carrier of M ; :: thesis: verum
end;
then reconsider Q = union { (Ball (x,r)) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) } as Subset of M by ZFMISC_1:76;
reconsider Q9 = Q as Subset of () ;
assume P in the topology of () ; :: thesis: ex Q being Subset of () st
( Q in the topology of () & P = Q /\ ([#] ()) )

then A1: P in Family_open_set A ;
A2: P c= Q9 /\ ([#] ())
proof
reconsider P9 = P as Subset of A ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P or a in Q9 /\ ([#] ()) )
assume A3: a in P ; :: thesis: a in Q9 /\ ([#] ())
then reconsider x = a as Point of A ;
reconsider x9 = x as Point of M by Th8;
consider r being Real such that
A4: r > 0 and
A5: Ball (x,r) c= P9 by ;
Ball (x,r) = (Ball (x9,r)) /\ the carrier of A by Th9;
then A6: Ball (x9,r) in { (Ball (x,r)) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) } by A3, A4, A5;
x9 in Ball (x9,r) by ;
then a in Q9 by ;
hence a in Q9 /\ ([#] ()) by ; :: thesis: verum
end;
take Q9 ; :: thesis: ( Q9 in the topology of () & P = Q9 /\ ([#] ()) )
for x being Point of M st x in Q holds
ex r being Real st
( r > 0 & Ball (x,r) c= Q )
proof
let x be Point of M; :: thesis: ( x in Q implies ex r being Real st
( r > 0 & Ball (x,r) c= Q ) )

assume x in Q ; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= Q )

then consider Y being set such that
A7: x in Y and
A8: Y in { (Ball (x,r)) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) } by TARSKI:def 4;
consider x9 being Point of M, r being Real such that
A9: Y = Ball (x9,r) and
x9 in P and
r > 0 and
(Ball (x9,r)) /\ the carrier of A c= P by A8;
consider p being Real such that
A10: p > 0 and
A11: Ball (x,p) c= Ball (x9,r) by ;
take p ; :: thesis: ( p > 0 & Ball (x,p) c= Q )
thus p > 0 by A10; :: thesis: Ball (x,p) c= Q
Y c= Q by ;
hence Ball (x,p) c= Q by ; :: thesis: verum
end;
then Q in Family_open_set M by PCOMPS_1:def 4;
hence Q9 in the topology of () ; :: thesis: P = Q9 /\ ([#] ())
Q9 /\ ([#] ()) c= P
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Q9 /\ ([#] ()) or a in P )
assume A12: a in Q9 /\ ([#] ()) ; :: thesis: a in P
then a in Q9 by XBOOLE_0:def 4;
then consider Y being set such that
A13: a in Y and
A14: Y in { (Ball (x,r)) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) } by TARSKI:def 4;
consider x being Point of M, r being Real such that
A15: Y = Ball (x,r) and
x in P and
r > 0 and
A16: (Ball (x,r)) /\ the carrier of A c= P by A14;
a in (Ball (x,r)) /\ the carrier of A by ;
hence a in P by A16; :: thesis: verum
end;
hence P = Q9 /\ ([#] ()) by ; :: thesis: verum
end;
reconsider P9 = P as Subset of A ;
given Q being Subset of () such that A17: Q in the topology of () and
A18: P = Q /\ ([#] ()) ; :: thesis: P in the topology of ()
reconsider Q9 = Q as Subset of M ;
for p being Point of A st p in P9 holds
ex r being Real st
( r > 0 & Ball (p,r) c= P9 )
proof
let p be Point of A; :: thesis: ( p in P9 implies ex r being Real st
( r > 0 & Ball (p,r) c= P9 ) )

reconsider p9 = p as Point of M by Th8;
assume p in P9 ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= P9 )

then A19: p9 in Q9 by ;
Q9 in Family_open_set M by A17;
then consider r being Real such that
A20: r > 0 and
A21: Ball (p9,r) c= Q9 by ;
Ball (p,r) = (Ball (p9,r)) /\ the carrier of A by Th9;
then Ball (p,r) c= Q /\ the carrier of A by ;
then Ball (p,r) c= Q /\ the carrier of () ;
hence ex r being Real st
( r > 0 & Ball (p,r) c= P9 ) by ; :: thesis: verum
end;
then P in Family_open_set A by PCOMPS_1:def 4;
hence P in the topology of () ; :: thesis: verum