let n be Nat; :: thesis: for T being non empty TopSpace st T is regular holds
( ( T is finite-ind & ind T <= n ) iff for A being closed Subset of T
for p being Point of T st not p in A holds
ex L being Subset of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 ) )
let T be non empty TopSpace; :: thesis: ( T is regular implies ( ( T is finite-ind & ind T <= n ) iff for A being closed Subset of T
for p being Point of T st not p in A holds
ex L being Subset of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 ) ) )
assume A1: T is regular ; :: thesis: ( ( T is finite-ind & ind T <= n ) iff for A being closed Subset of T
for p being Point of T st not p in A holds
ex L being Subset of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 ) )

hereby :: thesis: ( ( for A being closed Subset of T
for p being Point of T st not p in A holds
ex L being Subset of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 ) ) implies ( T is finite-ind & ind T <= n ) )

assume A2: ( T is finite-ind & ind T <= n ) ; :: thesis: for A being closed Subset of T
for p being Point of T st not p in A holds
ex L being Element of bool the carrier of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 )
let A be closed Subset of T; :: thesis: for p being Point of T st not p in A holds
ex L being Element of bool the carrier of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 )
let p be Point of T; :: thesis: ( not p in A implies ex L being Element of bool the carrier of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 ) )
assume not p in A ; :: thesis: ex L being Element of bool the carrier of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 )
then p in A ` by XBOOLE_0:def 5;
then consider V1, V2 being Subset of T such that
A3: V1 is open and
A4: V2 is open and
A5: p in V1 and
A6: A c= V2 and
A7: V1 misses V2 by A1, PRE_TOPC:def 11;
A8: V2 ` c= A ` by A6, SUBSET_1:12;
consider W1 being open Subset of T such that
A9: p in W1 and
A10: W1 c= V1 and
A11: ( Fr W1 is finite-ind & ind (Fr W1) <= n - 1 ) by A2, A3, A5, Th16;
take L = Fr W1; :: thesis: ( L separates {p},A & L is finite-ind & ind L <= n - 1 )
A12: L = (((Cl W1) \ W1) `) ` by TOPS_1:42
.= ((([#] T) \ (Cl W1)) \/ (([#] T) /\ W1)) ` by XBOOLE_1:52
.= (((Cl W1) `) \/ W1) ` by XBOOLE_1:28 ;
V2 misses Cl V1 by A4, A7, TSEP_1:36;
then A13: Cl V1 c= V2 ` by SUBSET_1:23;
Cl W1 c= Cl V1 by A10, PRE_TOPC:19;
then Cl W1 c= V2 ` by A13;
then Cl W1 c= A ` by A8;
then A14: A c= (Cl W1) ` by SUBSET_1:16;
W1 c= Cl W1 by PRE_TOPC:18;
then A15: (Cl W1) ` misses W1 by SUBSET_1:24;
{p} c= W1 by A9, ZFMISC_1:31;
hence ( L separates {p},A & L is finite-ind & ind L <= n - 1 ) by A11, A12, A14, A15, METRIZTS:def 3; :: thesis: verum

end;

assume A16: for A being closed Subset of T
for p being Point of T st not p in A holds
ex L being Subset of T st
( L separates {p},A & L is finite-ind & ind L <= n - 1 ) ; :: thesis: ( T is finite-ind & ind T <= n )
A17: for p being Point of T
for U being open Subset of T st p in U holds
ex W being open Subset of T st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )

proof

let p be Point of T; :: thesis: for U being open Subset of T st p in U holds
ex W being open Subset of T st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
let U be open Subset of T; :: thesis: ( p in U implies ex W being open Subset of T st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
assume p in U ; :: thesis: ex W being open Subset of T st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
then not p in U ` by XBOOLE_0:def 5;
then consider L being Subset of T such that
A18: L separates {p},U ` and
A19: L is finite-ind and
A20: ind L <= n - 1 by A16;
consider A1, A2 being open Subset of T such that
A21: {p} c= A1 and
A22: U ` c= A2 and
A23: A1 misses A2 and
A24: L = (A1 \/ A2) ` by A18, METRIZTS:def 3;
A25: ( A2 ` c= U & A1 c= A2 ` ) by A22, A23, SUBSET_1:17, SUBSET_1:23;
take A1 ; :: thesis: ( p in A1 & A1 c= U & Fr A1 is finite-ind & ind (Fr A1) <= n - 1 )
Cl A1 misses A2 by A23, TSEP_1:36;
then (Cl A1) \ A2 = Cl A1 by XBOOLE_1:83;
then Fr A1 = ((Cl A1) \ A2) \ A1 by TOPS_1:42
.= (Cl A1) \ (A2 \/ A1) by XBOOLE_1:41 ;
then A26: Fr A1 c= L by A24, XBOOLE_1:33;
then ind (Fr A1) <= ind L by A19, Th19;
hence ( p in A1 & A1 c= U & Fr A1 is finite-ind & ind (Fr A1) <= n - 1 ) by A19, A20, A21, A25, A26, Th19, XXREAL_0:2, ZFMISC_1:31; :: thesis: verum

end;

then T is finite-ind by Th15;
hence ( T is finite-ind & ind T <= n ) by A17, Th16; :: thesis: verum