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: TopSpaceMetr A is SubSpace of TopSpaceMetr M

set T = TopSpaceMetr M;

set R = TopSpaceMetr A;

thus [#] (TopSpaceMetr A) c= [#] (TopSpaceMetr M) by Def1; :: according to PRE_TOPC:def 4 :: thesis: for b_{1} being Element of bool the carrier of (TopSpaceMetr A) holds

( ( not b_{1} in the topology of (TopSpaceMetr A) or ex b_{2} being Element of bool the carrier of (TopSpaceMetr M) st

( b_{2} in the topology of (TopSpaceMetr M) & b_{1} = b_{2} /\ ([#] (TopSpaceMetr A)) ) ) & ( for b_{2} being Element of bool the carrier of (TopSpaceMetr M) holds

( not b_{2} in the topology of (TopSpaceMetr M) or not b_{1} = b_{2} /\ ([#] (TopSpaceMetr A)) ) or b_{1} in the topology of (TopSpaceMetr A) ) )

let P be Subset of (TopSpaceMetr A); :: thesis: ( ( not P in the topology of (TopSpaceMetr A) or ex b_{1} being Element of bool the carrier of (TopSpaceMetr M) st

( b_{1} in the topology of (TopSpaceMetr M) & P = b_{1} /\ ([#] (TopSpaceMetr A)) ) ) & ( for b_{1} being Element of bool the carrier of (TopSpaceMetr M) holds

( not b_{1} in the topology of (TopSpaceMetr M) or not P = b_{1} /\ ([#] (TopSpaceMetr A)) ) or P in the topology of (TopSpaceMetr A) ) )

thus ( P in the topology of (TopSpaceMetr A) implies ex Q being Subset of (TopSpaceMetr M) st

( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) ) ) :: thesis: ( for b_{1} being Element of bool the carrier of (TopSpaceMetr M) holds

( not b_{1} in the topology of (TopSpaceMetr M) or not P = b_{1} /\ ([#] (TopSpaceMetr A)) ) or P in the topology of (TopSpaceMetr A) )

given Q being Subset of (TopSpaceMetr M) such that A17: Q in the topology of (TopSpaceMetr M) and

A18: P = Q /\ ([#] (TopSpaceMetr A)) ; :: thesis: P in the topology of (TopSpaceMetr A)

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 )

hence P in the topology of (TopSpaceMetr A) ; :: thesis: verum

let A be non empty SubSpace of M; :: thesis: TopSpaceMetr A is SubSpace of TopSpaceMetr M

set T = TopSpaceMetr M;

set R = TopSpaceMetr A;

thus [#] (TopSpaceMetr A) c= [#] (TopSpaceMetr M) by Def1; :: according to PRE_TOPC:def 4 :: thesis: for b

( ( not b

( b

( not b

let P be Subset of (TopSpaceMetr A); :: thesis: ( ( not P in the topology of (TopSpaceMetr A) or ex b

( b

( not b

thus ( P in the topology of (TopSpaceMetr A) implies ex Q being Subset of (TopSpaceMetr M) st

( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) ) ) :: thesis: ( for b

( not b

proof

reconsider P9 = P as Subset of A ;
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

reconsider Q9 = Q as Subset of (TopSpaceMetr M) ;

assume P in the topology of (TopSpaceMetr A) ; :: thesis: ex Q being Subset of (TopSpaceMetr M) st

( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) )

then A1: P in Family_open_set A ;

A2: P c= Q9 /\ ([#] (TopSpaceMetr A))

for x being Point of M st x in Q holds

ex r being Real st

( r > 0 & Ball (x,r) c= Q )

hence Q9 in the topology of (TopSpaceMetr M) ; :: thesis: P = Q9 /\ ([#] (TopSpaceMetr A))

Q9 /\ ([#] (TopSpaceMetr A)) c= P

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

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

reconsider Q9 = Q as Subset of (TopSpaceMetr M) ;

assume P in the topology of (TopSpaceMetr A) ; :: thesis: ex Q being Subset of (TopSpaceMetr M) st

( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) )

then A1: P in Family_open_set A ;

A2: P c= Q9 /\ ([#] (TopSpaceMetr A))

proof

take
Q9
; :: thesis: ( Q9 in the topology of (TopSpaceMetr M) & P = Q9 /\ ([#] (TopSpaceMetr A)) )
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 /\ ([#] (TopSpaceMetr A)) )

assume A3: a in P ; :: thesis: a in Q9 /\ ([#] (TopSpaceMetr A))

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 A1, A3, PCOMPS_1:def 4;

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 A4, TBSP_1:11;

then a in Q9 by A6, TARSKI:def 4;

hence a in Q9 /\ ([#] (TopSpaceMetr A)) by A3, XBOOLE_0:def 4; :: thesis: verum

end;let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P or a in Q9 /\ ([#] (TopSpaceMetr A)) )

assume A3: a in P ; :: thesis: a in Q9 /\ ([#] (TopSpaceMetr A))

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 A1, A3, PCOMPS_1:def 4;

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 A4, TBSP_1:11;

then a in Q9 by A6, TARSKI:def 4;

hence a in Q9 /\ ([#] (TopSpaceMetr A)) by A3, XBOOLE_0:def 4; :: thesis: verum

for x being Point of M st x in Q holds

ex r being Real st

( r > 0 & Ball (x,r) c= Q )

proof

then
Q in Family_open_set M
by PCOMPS_1:def 4;
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 A7, A9, PCOMPS_1:27;

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 A8, ZFMISC_1:74;

hence Ball (x,p) c= Q by A9, A11; :: thesis: verum

end;( 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 A7, A9, PCOMPS_1:27;

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 A8, ZFMISC_1:74;

hence Ball (x,p) c= Q by A9, A11; :: thesis: verum

hence Q9 in the topology of (TopSpaceMetr M) ; :: thesis: P = Q9 /\ ([#] (TopSpaceMetr A))

Q9 /\ ([#] (TopSpaceMetr A)) c= P

proof

hence
P = Q9 /\ ([#] (TopSpaceMetr A))
by A2, XBOOLE_0:def 10; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Q9 /\ ([#] (TopSpaceMetr A)) or a in P )

assume A12: a in Q9 /\ ([#] (TopSpaceMetr A)) ; :: 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 A12, A13, A15, XBOOLE_0:def 4;

hence a in P by A16; :: thesis: verum

end;assume A12: a in Q9 /\ ([#] (TopSpaceMetr A)) ; :: 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 A12, A13, A15, XBOOLE_0:def 4;

hence a in P by A16; :: thesis: verum

given Q being Subset of (TopSpaceMetr M) such that A17: Q in the topology of (TopSpaceMetr M) and

A18: P = Q /\ ([#] (TopSpaceMetr A)) ; :: thesis: P in the topology of (TopSpaceMetr A)

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

then
P in Family_open_set A
by PCOMPS_1:def 4;
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 A18, XBOOLE_0:def 4;

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 A19, PCOMPS_1:def 4;

Ball (p,r) = (Ball (p9,r)) /\ the carrier of A by Th9;

then Ball (p,r) c= Q /\ the carrier of A by A21, XBOOLE_1:26;

then Ball (p,r) c= Q /\ the carrier of (TopSpaceMetr A) ;

hence ex r being Real st

( r > 0 & Ball (p,r) c= P9 ) by A18, A20; :: thesis: verum

end;( 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 A18, XBOOLE_0:def 4;

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 A19, PCOMPS_1:def 4;

Ball (p,r) = (Ball (p9,r)) /\ the carrier of A by Th9;

then Ball (p,r) c= Q /\ the carrier of A by A21, XBOOLE_1:26;

then Ball (p,r) c= Q /\ the carrier of (TopSpaceMetr A) ;

hence ex r being Real st

( r > 0 & Ball (p,r) c= P9 ) by A18, A20; :: thesis: verum

hence P in the topology of (TopSpaceMetr A) ; :: thesis: verum