let TM be metrizable TopSpace; :: thesis: for Null being Subset of st TM | Null is second-countable holds
( ( Null is with_finite_small_inductive_dimension & ind Null <= 0 ) iff for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Null misses Fr W ) )
let Null be Subset of ; :: thesis: ( TM | Null is second-countable implies ( ( Null is with_finite_small_inductive_dimension & ind Null <= 0 ) iff for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Null misses Fr W ) ) )
assume A1: TM | Null is second-countable ; :: thesis: ( ( Null is with_finite_small_inductive_dimension & ind Null <= 0 ) iff for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Null misses Fr W ) )

hereby :: thesis: ( ( for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Null misses Fr W ) ) implies ( Null is with_finite_small_inductive_dimension & ind Null <= 0 ) )

assume A2: ( Null is with_finite_small_inductive_dimension & ind Null <= 0 ) ; :: thesis: for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Null misses Fr W )
let p be Point of ; :: thesis: for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Null misses Fr W )
let U be open Subset of ; :: thesis: ( p in U implies ex W being open Subset of st
( p in W & W c= U & Null misses Fr W ) )
assume A3: p in U ; :: thesis: ex W being open Subset of st
( p in W & W c= U & Null misses Fr W )
reconsider P = {p} as Subset of by A3, ZFMISC_1:37;
not p in U ` by A3, XBOOLE_0:def 5;
then A4: P misses U ` by ZFMISC_1:56;
not TM is empty by A3;
then consider L being Subset of such that
A5: L separates P,U ` and
A6: L misses Null by A1, A2, A4, Th37;
consider W, W1 being open Subset of 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 & Null misses Fr W )
( W c= W1 ` & W1 ` c= (U ` ) ` ) by A8, A9, SUBSET_1:31, SUBSET_1:43;
hence ( p in W & W c= U ) by A7, XBOOLE_1:1, ZFMISC_1:37; :: thesis: Null misses Fr W
thus Null misses Fr W :: thesis: verum

proof

assume Null meets Fr W ; :: thesis: contradiction
then consider x being set such that
A11: x in Fr W and
A12: x in Null by XBOOLE_0:3;
Null c= L ` by A6, SUBSET_1:43;
then A13: ( x in W or x in W1 ) by A10, A12, XBOOLE_0:def 3;
A14: x in (Cl W) \ W by A11, TOPS_1:76;
then x in Cl W by XBOOLE_0:def 5;
then Cl W meets W1 by A13, A14, XBOOLE_0:3, XBOOLE_0:def 5;
hence contradiction by A9, TSEP_1:40; :: thesis: verum

end;

end;

set TN = TM | Null;
assume A15: for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Null misses Fr W ) ; :: thesis: ( Null is with_finite_small_inductive_dimension & ind Null <= 0 )
A16: for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )

proof

let p be Point of ; :: thesis: for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )
let U be open Subset of ; :: thesis: ( p in U implies ex W being open Subset of st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 ) )
assume A17: p in U ; :: thesis: ex W being open Subset of st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )
A18: [#] (TM | Null) = Null by PRE_TOPC:def 10;
then p in Null by A17;
then reconsider p' = p as Point of ;
consider U' being Subset of such that
A19: U' is open and
A20: U = U' /\ the carrier of (TM | Null) by TSP_1:def 1;
p' in U' by A17, A20, XBOOLE_0:def 4;
then consider W' being open Subset of such that
A21: ( p' in W' & W' c= U' ) and
A22: Null misses Fr W' by A15, A19;
reconsider W = W' /\ the carrier of (TM | Null) as Subset of by XBOOLE_1:17;
reconsider W = W as open Subset of by TSP_1:def 1;
take W ; :: thesis: ( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )
thus ( p in W & W c= U ) by A17, A20, A21, XBOOLE_0:def 4, XBOOLE_1:26; :: thesis: ( Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )
A23: (Fr W') /\ Null = {} by A22, XBOOLE_0:def 7;
Fr W c= (Fr W') /\ Null by A18, Th1;
hence ( Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 ) by A23, Th6; :: thesis: verum

end;

then A24: TM | Null is with_finite_small_inductive_dimension by Th15;
then A25: Null is with_finite_small_inductive_dimension by Th18;
ind (TM | Null) <= 0 by A16, A24, Th16;
hence ( Null is with_finite_small_inductive_dimension & ind Null <= 0 ) by A25, Lm5; :: thesis: verum