let n be Nat; :: thesis: for TM being metrizable TopSpace

for H being Subset of TM st TM | H is second-countable holds

( ( H is finite-ind & ind H <= n ) iff for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) )

let TM be metrizable TopSpace; :: thesis: for H being Subset of TM st TM | H is second-countable holds

( ( H is finite-ind & ind H <= n ) iff for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) )

let M be Subset of TM; :: thesis: ( TM | M is second-countable implies ( ( M is finite-ind & ind M <= n ) iff for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

assume A1: TM | M is second-countable ; :: thesis: ( ( M is finite-ind & ind M <= n ) iff for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) )

assume A13: for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ; :: thesis: ( M is finite-ind & ind M <= n )

A14: for p being Point of (TM | M)

for U being open Subset of (TM | M) st p in U holds

ex W being open Subset of (TM | M) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

then A25: M is finite-ind by TOPDIM_1:18;

ind (TM | M) <= n by A14, A24, TOPDIM_1:16;

hence ( M is finite-ind & ind M <= n ) by A25, TOPDIM_1:17; :: thesis: verum

for H being Subset of TM st TM | H is second-countable holds

( ( H is finite-ind & ind H <= n ) iff for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) )

let TM be metrizable TopSpace; :: thesis: for H being Subset of TM st TM | H is second-countable holds

( ( H is finite-ind & ind H <= n ) iff for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) )

let M be Subset of TM; :: thesis: ( TM | M is second-countable implies ( ( M is finite-ind & ind M <= n ) iff for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

assume A1: TM | M is second-countable ; :: thesis: ( ( M is finite-ind & ind M <= n ) iff for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) )

hereby :: thesis: ( ( for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) implies ( M is finite-ind & ind M <= n ) )

set Tm = TM | M;for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) implies ( M is finite-ind & ind M <= n ) )

assume that

A2: M is finite-ind and

A3: ind M <= n ; :: thesis: for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

let p be Point of TM; :: thesis: for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

let U be open Subset of TM; :: thesis: ( p in U implies ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) )

assume A4: p in U ; :: thesis: ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

reconsider P = {p} as Subset of TM by A4, ZFMISC_1:31;

( not TM is empty & not p in U ` ) by A4, XBOOLE_0:def 5;

then consider L being Subset of TM such that

A5: L separates P,U ` and

A6: ind (L /\ M) <= n - 1 by A1, A2, A3, Th11, ZFMISC_1:50;

consider W, W1 being open Subset of TM such that

A7: P c= W and

A8: U ` c= W1 and

A9: W misses W1 and

A10: L = (W \/ W1) ` by A5, METRIZTS:def 3;

take W = W; :: thesis: ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

( W c= W1 ` & W1 ` c= (U `) ` ) by A8, A9, SUBSET_1:12, SUBSET_1:23;

hence ( p in W & W c= U ) by A7, ZFMISC_1:31; :: thesis: ( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

Cl W misses W1 by A9, TSEP_1:36;

then (Cl W) \ W1 = Cl W by XBOOLE_1:83;

then Fr W = ((Cl W) \ W1) \ W by TOPS_1:42

.= (Cl W) \ (W \/ W1) by XBOOLE_1:41

.= (Cl W) /\ L by A10, SUBSET_1:13 ;

then Fr W c= L by XBOOLE_1:17;

then A11: M /\ (Fr W) c= M /\ L by XBOOLE_1:27;

M /\ L c= M by XBOOLE_1:17;

then A12: M /\ L is finite-ind by A2, TOPDIM_1:19;

then ind (M /\ (Fr W)) <= ind (M /\ L) by A11, TOPDIM_1:19;

hence ( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A6, A11, A12, TOPDIM_1:19, XXREAL_0:2; :: thesis: verum

end;A2: M is finite-ind and

A3: ind M <= n ; :: thesis: for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

let p be Point of TM; :: thesis: for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

let U be open Subset of TM; :: thesis: ( p in U implies ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) )

assume A4: p in U ; :: thesis: ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

reconsider P = {p} as Subset of TM by A4, ZFMISC_1:31;

( not TM is empty & not p in U ` ) by A4, XBOOLE_0:def 5;

then consider L being Subset of TM such that

A5: L separates P,U ` and

A6: ind (L /\ M) <= n - 1 by A1, A2, A3, Th11, ZFMISC_1:50;

consider W, W1 being open Subset of TM such that

A7: P c= W and

A8: U ` c= W1 and

A9: W misses W1 and

A10: L = (W \/ W1) ` by A5, METRIZTS:def 3;

take W = W; :: thesis: ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

( W c= W1 ` & W1 ` c= (U `) ` ) by A8, A9, SUBSET_1:12, SUBSET_1:23;

hence ( p in W & W c= U ) by A7, ZFMISC_1:31; :: thesis: ( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

Cl W misses W1 by A9, TSEP_1:36;

then (Cl W) \ W1 = Cl W by XBOOLE_1:83;

then Fr W = ((Cl W) \ W1) \ W by TOPS_1:42

.= (Cl W) \ (W \/ W1) by XBOOLE_1:41

.= (Cl W) /\ L by A10, SUBSET_1:13 ;

then Fr W c= L by XBOOLE_1:17;

then A11: M /\ (Fr W) c= M /\ L by XBOOLE_1:27;

M /\ L c= M by XBOOLE_1:17;

then A12: M /\ L is finite-ind by A2, TOPDIM_1:19;

then ind (M /\ (Fr W)) <= ind (M /\ L) by A11, TOPDIM_1:19;

hence ( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A6, A11, A12, TOPDIM_1:19, XXREAL_0:2; :: thesis: verum

assume A13: for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ; :: thesis: ( M is finite-ind & ind M <= n )

A14: for p being Point of (TM | M)

for U being open Subset of (TM | M) st p in U holds

ex W being open Subset of (TM | M) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

proof

then A24:
TM | M is finite-ind
by TOPDIM_1:15;
A15:
[#] (TM | M) = M
by PRE_TOPC:def 5;

let p be Point of (TM | M); :: thesis: for U being open Subset of (TM | M) st p in U holds

ex W being open Subset of (TM | M) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

let U be open Subset of (TM | M); :: thesis: ( p in U implies ex W being open Subset of (TM | M) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )

assume A16: p in U ; :: thesis: ex W being open Subset of (TM | M) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

p in M by A15, A16;

then reconsider p9 = p as Point of TM ;

consider U9 being Subset of TM such that

A17: U9 is open and

A18: U = U9 /\ the carrier of (TM | M) by TSP_1:def 1;

p9 in U9 by A16, A18, XBOOLE_0:def 4;

then consider W9 being open Subset of TM such that

A19: ( p9 in W9 & W9 c= U9 ) and

A20: M /\ (Fr W9) is finite-ind and

A21: ind (M /\ (Fr W9)) <= n - 1 by A13, A17;

reconsider W = W9 /\ the carrier of (TM | M) as Subset of (TM | M) by XBOOLE_1:17;

reconsider W = W as open Subset of (TM | M) by TSP_1:def 1;

take W ; :: thesis: ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

thus ( p in W & W c= U ) by A16, A18, A19, XBOOLE_0:def 4, XBOOLE_1:26; :: thesis: ( Fr W is finite-ind & ind (Fr W) <= n - 1 )

reconsider FrW = Fr W as Subset of TM by A15, XBOOLE_1:1;

A22: FrW c= (Fr W9) /\ M by A15, TOPDIM_1:1;

then A23: FrW is finite-ind by A20, TOPDIM_1:19;

ind FrW <= ind ((Fr W9) /\ M) by A20, A22, TOPDIM_1:19;

then ind (Fr W) <= ind ((Fr W9) /\ M) by A23, TOPDIM_1:21;

hence ( Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A21, A23, TOPDIM_1:21, XXREAL_0:2; :: thesis: verum

end;let p be Point of (TM | M); :: thesis: for U being open Subset of (TM | M) st p in U holds

ex W being open Subset of (TM | M) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

let U be open Subset of (TM | M); :: thesis: ( p in U implies ex W being open Subset of (TM | M) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )

assume A16: p in U ; :: thesis: ex W being open Subset of (TM | M) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

p in M by A15, A16;

then reconsider p9 = p as Point of TM ;

consider U9 being Subset of TM such that

A17: U9 is open and

A18: U = U9 /\ the carrier of (TM | M) by TSP_1:def 1;

p9 in U9 by A16, A18, XBOOLE_0:def 4;

then consider W9 being open Subset of TM such that

A19: ( p9 in W9 & W9 c= U9 ) and

A20: M /\ (Fr W9) is finite-ind and

A21: ind (M /\ (Fr W9)) <= n - 1 by A13, A17;

reconsider W = W9 /\ the carrier of (TM | M) as Subset of (TM | M) by XBOOLE_1:17;

reconsider W = W as open Subset of (TM | M) by TSP_1:def 1;

take W ; :: thesis: ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

thus ( p in W & W c= U ) by A16, A18, A19, XBOOLE_0:def 4, XBOOLE_1:26; :: thesis: ( Fr W is finite-ind & ind (Fr W) <= n - 1 )

reconsider FrW = Fr W as Subset of TM by A15, XBOOLE_1:1;

A22: FrW c= (Fr W9) /\ M by A15, TOPDIM_1:1;

then A23: FrW is finite-ind by A20, TOPDIM_1:19;

ind FrW <= ind ((Fr W9) /\ M) by A20, A22, TOPDIM_1:19;

then ind (Fr W) <= ind ((Fr W9) /\ M) by A23, TOPDIM_1:21;

hence ( Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A21, A23, TOPDIM_1:21, XXREAL_0:2; :: thesis: verum

then A25: M is finite-ind by TOPDIM_1:18;

ind (TM | M) <= n by A14, A24, TOPDIM_1:16;

hence ( M is finite-ind & ind M <= n ) by A25, TOPDIM_1:17; :: thesis: verum