end;

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

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

end;