:: TOPDIM_1 semantic presentation

begin


theorem Th1: :: TOPDIM_1:1
for T being TopSpace
for B, A being Subset of T
for F being Subset of (T | A) st F = B /\ A holds
Fr F c= (Fr B) /\ A
proof
let T be TopSpace; ::_thesis: for B, A being Subset of T
for F being Subset of (T | A) st F = B /\ A holds
Fr F c= (Fr B) /\ A
let B, A be Subset of T; ::_thesis: for F being Subset of (T | A) st F = B /\ A holds
Fr F c= (Fr B) /\ A
let F be Subset of (T | A); ::_thesis: ( F = B /\ A implies Fr F c= (Fr B) /\ A )
A1: [#] (T | A) = A by PRE_TOPC:def_5;
 [#] (T | A) c= [#] T by PRE_TOPC:def_4;
then reconsider F9 = F, Fd = F ` as Subset of T by XBOOLE_1:1;
assume A2: F = B /\ A ; ::_thesis: Fr F c= (Fr B) /\ A
then  Cl F9 c= Cl B by PRE_TOPC:19, XBOOLE_1:18;
then  (Cl F9) /\ A c= (Cl B) /\ A by XBOOLE_1:26;
then A3: Cl F c= (Cl B) /\ A by A1, PRE_TOPC:17;
 [#] (T | A) = A by PRE_TOPC:def_5;
then  F ` = A \ B by A2, XBOOLE_1:47;
then  F ` c= B ` by XBOOLE_1:35;
then  Cl Fd c= Cl (B `) by PRE_TOPC:19;
then A4: (Cl Fd) /\ A c= (Cl (B `)) /\ A by XBOOLE_1:26;
 Cl (F `) = (Cl Fd) /\ ([#] (T | A)) by PRE_TOPC:17;
then  Cl (F `) c= Cl (B `) by A1, A4, XBOOLE_1:18;
then  (Cl F) /\ (Cl (F `)) c= ((Cl B) /\ A) /\ (Cl (B `)) by A3, XBOOLE_1:27;
hence  Fr F c= (Fr B) /\ A by XBOOLE_1:16; ::_thesis: verum
end;

theorem Th2: :: TOPDIM_1:2
for T being TopSpace holds
( T is normal iff for A, B being closed Subset of T st A misses B holds
ex U, W being open Subset of T st
( A c= U & B c= W & Cl U misses Cl W ) )
proof
let T be TopSpace; ::_thesis: ( T is normal iff for A, B being closed Subset of T st A misses B holds
ex U, W being open Subset of T st
( A c= U & B c= W & Cl U misses Cl W ) )
hereby  ::_thesis: ( ( for A, B being closed Subset of T st A misses B holds
ex U, W being open Subset of T st
( A c= U & B c= W & Cl U misses Cl W ) ) implies T is normal )
assume A1: T is normal ; ::_thesis: for A1, A2 being closed Subset of T st A1 misses A2 holds
ex C1, D1 being open Subset of T st
( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 )
let A1, A2 be closed Subset of T; ::_thesis: ( A1 misses A2 implies ex C1, D1 being open Subset of T st
( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 ) )
assume  A1 misses A2 ; ::_thesis: ex C1, D1 being open Subset of T st
( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 )
then consider B1, B2 being Subset of T such that
A2: B1 is open and
A3: B2 is open and
A4: A1 c= B1 and
A5: A2 c= B2 and
A6: B1 misses B2 by A1, PRE_TOPC:def_12;
 A1 misses B1 ` by A4, SUBSET_1:24;
then consider C1, C2 being Subset of T such that
A7: C1 is open and
A8: C2 is open and
A9: A1 c= C1 and
A10: B1 ` c= C2 and
A11: C1 misses C2 by A1, A2, PRE_TOPC:def_12;
A12: ( Cl (C2 `) = C2 ` & C2 ` c= B1 ) by A8, A10, PRE_TOPC:22, SUBSET_1:17;
 A2 misses B2 ` by A5, SUBSET_1:24;
then consider D1, D2 being Subset of T such that
A13: D1 is open and
A14: D2 is open and
A15: A2 c= D1 and
A16: B2 ` c= D2 and
A17: D1 misses D2 by A1, A3, PRE_TOPC:def_12;
reconsider C1 = C1, D1 = D1 as open Subset of T by A13, A7;
take C1 = C1; ::_thesis: ex D1 being open Subset of T st
( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 )
take D1 = D1; ::_thesis: ( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 )
 D1 c= D2 ` by A17, SUBSET_1:23;
then A18: Cl D1 c= Cl (D2 `) by PRE_TOPC:19;
 C1 c= C2 ` by A11, SUBSET_1:23;
then  Cl C1 c= Cl (C2 `) by PRE_TOPC:19;
then A19: Cl C1 c= B1 by A12, XBOOLE_1:1;
 ( Cl (D2 `) = D2 ` & D2 ` c= B2 ) by A14, A16, PRE_TOPC:22, SUBSET_1:17;
then  Cl D1 c= B2 by A18, XBOOLE_1:1;
hence  ( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 ) by A6, A15, A9, A19, XBOOLE_1:64; ::_thesis: verum
end;
assume A20: for A, B being closed Subset of T st A misses B holds
ex U, W being open Subset of T st
( A c= U & B c= W & Cl U misses Cl W ) ; ::_thesis: T is normal
 for A, B being Subset of T st A is closed & B is closed & A misses B holds
ex U, W being Subset of T st
( U is open & W is open & A c= U & B c= W & U misses W )
proof
let A, B be Subset of T; ::_thesis: ( A is closed & B is closed & A misses B implies ex U, W being Subset of T st
( U is open & W is open & A c= U & B c= W & U misses W ) )
assume  ( A is closed & B is closed & A misses B ) ; ::_thesis: ex U, W being Subset of T st
( U is open & W is open & A c= U & B c= W & U misses W )
then consider U, W being open Subset of T such that
A21: ( A c= U & B c= W & Cl U misses Cl W ) by A20;
take  U ; ::_thesis: ex W being Subset of T st
( U is open & W is open & A c= U & B c= W & U misses W )
take  W ; ::_thesis: ( U is open & W is open & A c= U & B c= W & U misses W )
 ( U c= Cl U & W c= Cl W ) by PRE_TOPC:18;
hence  ( U is open & W is open & A c= U & B c= W & U misses W ) by A21, XBOOLE_1:64; ::_thesis: verum
end;
hence  T is normal by PRE_TOPC:def_12; ::_thesis: verum
end;

definition
let T be TopSpace;
func Seq_of_ind T ->  SetSequence of (bool the carrier of T) means :Def1: :: TOPDIM_1:def 1
 for A being Subset of T
for n being Nat holds
( it . 0 = {({} T)} & ( not A in it . (n + 1) or A in it . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in it . n ) ) & ( ( A in it . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in it . n ) ) implies A in it . (n + 1) ) );
existence
 ex b1 being SetSequence of (bool the carrier of T) st
for A being Subset of T
for n being Nat holds
( b1 . 0 = {({} T)} & ( not A in b1 . (n + 1) or A in b1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b1 . n ) ) & ( ( A in b1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b1 . n ) ) implies A in b1 . (n + 1) ) )
proof
defpred S1[ set , set ] means  for A being Subset of T holds
( A in $2 iff ( A in $1 or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in $1 ) ) );
set C = the carrier of T;
reconsider E = {({} T)} as Element of bool (bool the carrier of T) ;
A1: for x being set st x in bool (bool the carrier of T) holds
ex y being set st
( y in bool (bool the carrier of T) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in bool (bool the carrier of T) implies ex y being set st
( y in bool (bool the carrier of T) & S1[x,y] ) )
assume  x in bool (bool the carrier of T) ; ::_thesis: ex y being set st
( y in bool (bool the carrier of T) & S1[x,y] )
defpred S2[ set ] means  for A being Subset of T holds
( not A = $1 or A in x or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in x ) );
consider y being Subset of (bool the carrier of T) such that
A2: for z being set holds
( z in y iff ( z in bool the carrier of T & S2[z] ) ) from SUBSET_1:sch_1();
take  y ; ::_thesis: ( y in bool (bool the carrier of T) & S1[x,y] )
thus  y in bool (bool the carrier of T) ; ::_thesis: S1[x,y]
let A be Subset of T; ::_thesis: ( A in y iff ( A in x or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in x ) ) )
 ( A in y iff S2[A] ) by A2;
hence  ( A in y iff ( A in x or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in x ) ) ) ; ::_thesis: verum
end;
consider p being Function of (bool (bool the carrier of T)),(bool (bool the carrier of T)) such that
A3: for x being set st x in bool (bool the carrier of T) holds
S1[x,p . x] from FUNCT_2:sch_1(A1);
deffunc H1( set , set ) ->  Element of bool (bool the carrier of T) = p /. $2;
consider f being Function of NAT,(bool (bool the carrier of T)) such that
A4: f . 0 = E and
A5: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_12();
reconsider f = f as SetSequence of (bool the carrier of T) ;
take  f ; ::_thesis: for A being Subset of T
for n being Nat holds
( f . 0 = {({} T)} & ( not A in f . (n + 1) or A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) & ( ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) implies A in f . (n + 1) ) )
now__::_thesis:_for_n_being_Nat
for_A_being_Subset_of_T_holds_
(_A_in_f_._(n_+_1)_iff_(_A_in_f_._n_or_for_p_being_Point_of_(T_|_A)
for_U_being_open_Subset_of_(T_|_A)_st_p_in_U_holds_
ex_W_being_open_Subset_of_(T_|_A)_st_
(_p_in_W_&_W_c=_U_&_Fr_W_in_f_._n_)_)_)
let n be Nat; ::_thesis: for A being Subset of T holds
( A in f . (n + 1) iff ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) )
f . (n + 1) = p /. (f . n) by A5
.= p . (f . n) ;
hence  for A being Subset of T holds
( A in f . (n + 1) iff ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) ) by A3; ::_thesis: verum
end;
hence  for A being Subset of T
for n being Nat holds
( f . 0 = {({} T)} & ( not A in f . (n + 1) or A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) & ( ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) implies A in f . (n + 1) ) ) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of (bool the carrier of T) st ( for A being Subset of T
for n being Nat holds
( b1 . 0 = {({} T)} & ( not A in b1 . (n + 1) or A in b1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b1 . n ) ) & ( ( A in b1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b1 . n ) ) implies A in b1 . (n + 1) ) ) ) & ( for A being Subset of T
for n being Nat holds
( b2 . 0 = {({} T)} & ( not A in b2 . (n + 1) or A in b2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b2 . n ) ) & ( ( A in b2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b2 . n ) ) implies A in b2 . (n + 1) ) ) ) holds
b1 = b2
proof
let Ind1, Ind2 be SetSequence of (bool the carrier of T); ::_thesis: ( ( for A being Subset of T
for n being Nat holds
( Ind1 . 0 = {({} T)} & ( not A in Ind1 . (n + 1) or A in Ind1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind1 . n ) ) & ( ( A in Ind1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind1 . n ) ) implies A in Ind1 . (n + 1) ) ) ) & ( for A being Subset of T
for n being Nat holds
( Ind2 . 0 = {({} T)} & ( not A in Ind2 . (n + 1) or A in Ind2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind2 . n ) ) & ( ( A in Ind2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind2 . n ) ) implies A in Ind2 . (n + 1) ) ) ) implies Ind1 = Ind2 )
assume that
A6: for A being Subset of T
for n being Nat holds
( Ind1 . 0 = {({} T)} & ( not A in Ind1 . (n + 1) or A in Ind1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind1 . n ) ) & ( ( A in Ind1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind1 . n ) ) implies A in Ind1 . (n + 1) ) ) and
A7: for A being Subset of T
for n being Nat holds
( Ind2 . 0 = {({} T)} & ( not A in Ind2 . (n + 1) or A in Ind2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind2 . n ) ) & ( ( A in Ind2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind2 . n ) ) implies A in Ind2 . (n + 1) ) ) ; ::_thesis: Ind1 = Ind2
defpred S1[ Nat] means Ind1 . $1 = Ind2 . $1;
A8: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A9: S1[n] ; ::_thesis: S1[n + 1]
thus  Ind1 . (n + 1) c= Ind2 . (n + 1) :: according to XBOOLE_0:def_10 ::_thesis: Ind2 . (n + 1) c= Ind1 . (n + 1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ind1 . (n + 1) or x in Ind2 . (n + 1) )
assume A10: x in Ind1 . (n + 1) ; ::_thesis: x in Ind2 . (n + 1)
reconsider A = x as Subset of T by A10;
 ( A in Ind1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind1 . n ) ) by A6, A10;
hence  x in Ind2 . (n + 1) by A7, A9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ind2 . (n + 1) or x in Ind1 . (n + 1) )
assume A11: x in Ind2 . (n + 1) ; ::_thesis: x in Ind1 . (n + 1)
reconsider A = x as Subset of T by A11;
 ( A in Ind2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in Ind2 . n ) ) by A7, A11;
hence  x in Ind1 . (n + 1) by A6, A9; ::_thesis: verum
end;
A12: S1[ 0 ] by A6, A7;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A12, A8);
hence  Ind1 = Ind2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def_1_:_
 for T being TopSpace
for b2 being SetSequence of (bool the carrier of T) holds
( b2 = Seq_of_ind T iff for A being Subset of T
for n being Nat holds
( b2 . 0 = {({} T)} & ( not A in b2 . (n + 1) or A in b2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b2 . n ) ) & ( ( A in b2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b2 . n ) ) implies A in b2 . (n + 1) ) ) );

registration
let T be TopSpace;
cluster Seq_of_ind T ->  non-descending ;
coherence
 Seq_of_ind T is non-descending
proof
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Seq_of_ind_T)_._n_c=_(Seq_of_ind_T)_._(n_+_1)
let n be Element of NAT ; ::_thesis: (Seq_of_ind T) . n c= (Seq_of_ind T) . (n + 1)
thus  (Seq_of_ind T) . n c= (Seq_of_ind T) . (n + 1) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Seq_of_ind T) . n or x in (Seq_of_ind T) . (n + 1) )
assume  x in (Seq_of_ind T) . n ; ::_thesis: x in (Seq_of_ind T) . (n + 1)
hence  x in (Seq_of_ind T) . (n + 1) by Def1; ::_thesis: verum
end;
end;
hence  Seq_of_ind T is non-descending by KURATO_0:def_4; ::_thesis: verum
end;
end;

theorem Th3: :: TOPDIM_1:3
for T being TopSpace
for A, B being Subset of T
for n being Nat
for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T
for n being Nat
for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )
let A, B be Subset of T; ::_thesis: for n being Nat
for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )
let n be Nat; ::_thesis: for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )
defpred S1[ Nat] means  for F being Subset of (T | A)
for B being Subset of T st F = B holds
( F in (Seq_of_ind (T | A)) . $1 iff B in (Seq_of_ind T) . $1 );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
set TA = T | A;
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
set n1 = n + 1;
let F be Subset of (T | A); ::_thesis: for B being Subset of T st F = B holds
( F in (Seq_of_ind (T | A)) . (n + 1) iff B in (Seq_of_ind T) . (n + 1) )
let B be Subset of T; ::_thesis: ( F = B implies ( F in (Seq_of_ind (T | A)) . (n + 1) iff B in (Seq_of_ind T) . (n + 1) ) )
assume A3: F = B ; ::_thesis: ( F in (Seq_of_ind (T | A)) . (n + 1) iff B in (Seq_of_ind T) . (n + 1) )
set TAF = (T | A) | F;
set TB = T | B;
A4: (T | A) | F = T | B by A3, METRIZTS:9;
A5: [#] (T | B) c= [#] T by PRE_TOPC:def_4;
hereby  ::_thesis: ( B in (Seq_of_ind T) . (n + 1) implies F in (Seq_of_ind (T | A)) . (n + 1) )
assume A6: F in (Seq_of_ind (T | A)) . (n + 1) ; ::_thesis: B in (Seq_of_ind T) . (n + 1)
percases ( F in (Seq_of_ind (T | A)) . n or for p being Point of ((T | A) | F)
for U being open Subset of ((T | A) | F) st p in U holds
ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n ) ) by A6, Def1;
suppose F in (Seq_of_ind (T | A)) . n ; ::_thesis: B in (Seq_of_ind T) . (n + 1)
then  B in (Seq_of_ind T) . n by A2, A3;
hence  B in (Seq_of_ind T) . (n + 1) by Def1; ::_thesis: verum
end;
supposeA7: for p being Point of ((T | A) | F)
for U being open Subset of ((T | A) | F) st p in U holds
ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n ) ; ::_thesis: B in (Seq_of_ind T) . (n + 1)
now__::_thesis:_for_p_being_Point_of_(T_|_B)
for_U_being_open_Subset_of_(T_|_B)_st_p_in_U_holds_
ex_W_being_open_Subset_of_(T_|_B)_st_
(_p_in_W_&_W_c=_U_&_Fr_W_in_(Seq_of_ind_T)_._n_)
let p be Point of (T | B); ::_thesis: for U being open Subset of (T | B) st p in U holds
ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
let U be open Subset of (T | B); ::_thesis: ( p in U implies ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) )
assume A8: p in U ; ::_thesis: ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
reconsider U9 = U as open Subset of ((T | A) | F) by A4;
consider W9 being open Subset of ((T | A) | F) such that
A9: ( p in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind (T | A)) . n ) by A7, A8;
reconsider W = W9 as open Subset of (T | B) by A4;
take W = W; ::_thesis: ( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
 Fr W is Subset of T by A5, XBOOLE_1:1;
hence  ( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) by A2, A4, A9; ::_thesis: verum
end;
hence  B in (Seq_of_ind T) . (n + 1) by Def1; ::_thesis: verum
end;
end;
end;
A10: [#] ((T | A) | F) c= [#] (T | A) by PRE_TOPC:def_4;
assume A11: B in (Seq_of_ind T) . (n + 1) ; ::_thesis: F in (Seq_of_ind (T | A)) . (n + 1)
percases ( B in (Seq_of_ind T) . n or for p being Point of (T | B)
for U being open Subset of (T | B) st p in U holds
ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) ) by A11, Def1;
suppose B in (Seq_of_ind T) . n ; ::_thesis: F in (Seq_of_ind (T | A)) . (n + 1)
then  F in (Seq_of_ind (T | A)) . n by A2, A3;
hence  F in (Seq_of_ind (T | A)) . (n + 1) by Def1; ::_thesis: verum
end;
supposeA12: for p being Point of (T | B)
for U being open Subset of (T | B) st p in U holds
ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) ; ::_thesis: F in (Seq_of_ind (T | A)) . (n + 1)
now__::_thesis:_for_p_being_Point_of_((T_|_A)_|_F)
for_U_being_open_Subset_of_((T_|_A)_|_F)_st_p_in_U_holds_
ex_W_being_open_Subset_of_((T_|_A)_|_F)_st_
(_p_in_W_&_W_c=_U_&_Fr_W_in_(Seq_of_ind_(T_|_A))_._n_)
let p be Point of ((T | A) | F); ::_thesis: for U being open Subset of ((T | A) | F) st p in U holds
ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n )
let U be open Subset of ((T | A) | F); ::_thesis: ( p in U implies ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n ) )
assume A13: p in U ; ::_thesis: ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n )
reconsider U9 = U as open Subset of (T | B) by A4;
consider W9 being open Subset of (T | B) such that
A14: ( p in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind T) . n ) by A12, A13;
reconsider W = W9 as open Subset of ((T | A) | F) by A4;
take W = W; ::_thesis: ( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n )
 Fr W is Subset of (T | A) by A10, XBOOLE_1:1;
hence  ( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n ) by A2, A4, A14; ::_thesis: verum
end;
hence  F in (Seq_of_ind (T | A)) . (n + 1) by Def1; ::_thesis: verum
end;
end;
end;
A15: S1[ 0 ]
proof
A16: (Seq_of_ind (T | A)) . 0 = {({} (T | A))} by Def1
.= {({} T)}
.= (Seq_of_ind T) . 0 by Def1 ;
let F be Subset of (T | A); ::_thesis: for B being Subset of T st F = B holds
( F in (Seq_of_ind (T | A)) . 0 iff B in (Seq_of_ind T) . 0 )
let B be Subset of T; ::_thesis: ( F = B implies ( F in (Seq_of_ind (T | A)) . 0 iff B in (Seq_of_ind T) . 0 ) )
assume  F = B ; ::_thesis: ( F in (Seq_of_ind (T | A)) . 0 iff B in (Seq_of_ind T) . 0 )
hence  ( F in (Seq_of_ind (T | A)) . 0 iff B in (Seq_of_ind T) . 0 ) by A16; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A15, A1);
hence  for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n ) ; ::_thesis: verum
end;

definition
let T be TopSpace;
let A be Subset of T;
attrA is with_finite_small_inductive_dimension  means :Def2: :: TOPDIM_1:def 2
 ex n being Nat st A in (Seq_of_ind T) . n;
end;

:: deftheorem Def2 defines with_finite_small_inductive_dimension TOPDIM_1:def_2_:_
 for T being TopSpace
for A being Subset of T holds
( A is with_finite_small_inductive_dimension iff ex n being Nat st A in (Seq_of_ind T) . n );

notation
let T be TopSpace;
let A be Subset of T;
synonym  finite-ind A for  with_finite_small_inductive_dimension ;
end;

definition
let T be TopSpace;
let G be Subset-Family of T;
attrG is with_finite_small_inductive_dimension  means :Def3: :: TOPDIM_1:def 3
 ex n being Nat st G c= (Seq_of_ind T) . n;
end;

:: deftheorem Def3 defines with_finite_small_inductive_dimension TOPDIM_1:def_3_:_
 for T being TopSpace
for G being Subset-Family of T holds
( G is with_finite_small_inductive_dimension iff ex n being Nat st G c= (Seq_of_ind T) . n );

notation
let T be TopSpace;
let G be Subset-Family of T;
synonym  finite-ind G for  with_finite_small_inductive_dimension ;
end;

theorem Th4: :: TOPDIM_1:4
for T being TopSpace
for A being Subset of T
for G being Subset-Family of T st A in G & G is finite-ind holds
A is finite-ind
proof
let T be TopSpace; ::_thesis: for A being Subset of T
for G being Subset-Family of T st A in G & G is finite-ind holds
A is finite-ind
let A be Subset of T; ::_thesis: for G being Subset-Family of T st A in G & G is finite-ind holds
A is finite-ind
let G be Subset-Family of T; ::_thesis: ( A in G & G is finite-ind implies A is finite-ind )
assume that
A1: A in G and
A2: G is finite-ind ; ::_thesis: A is finite-ind
 ex n being Nat st G c= (Seq_of_ind T) . n by A2, Def3;
hence  A is finite-ind by A1, Def2; ::_thesis: verum
end;

Lm1:  for T being TopSpace
for A being finite Subset of T holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )
proof
defpred S1[ Nat] means  for T being TopSpace
for A being finite Subset of T st card A <= $1 holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) );
let T be TopSpace; ::_thesis: for A being finite Subset of T holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )
let A be finite Subset of T; ::_thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let T be TopSpace; ::_thesis: for A being finite Subset of T st card A <= n + 1 holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )
let A be finite Subset of T; ::_thesis: ( card A <= n + 1 implies ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) )
assume A3: card A <= n + 1 ; ::_thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )
percases ( card A <= n or card A = n + 1 ) by A3, NAT_1:8;
suppose card A <= n ; ::_thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )
hence  ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) by A2; ::_thesis: verum
end;
supposeA4: card A = n + 1 ; ::_thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )
 for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
proof
let p be Point of (T | A); ::_thesis: for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
let U be open Subset of (T | A); ::_thesis: ( p in U implies ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) )
assume A5: p in U ; ::_thesis: ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
take W = U; ::_thesis: ( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
 {p} c= W by A5, ZFMISC_1:31;
then A6: ( Fr W = (Cl W) \ W & A \ W c= A \ {p} ) by TOPS_1:42, XBOOLE_1:34;
thus  ( p in W & W c= U ) by A5; ::_thesis: Fr W in (Seq_of_ind T) . n
 [#] (T | A) c= [#] T by PRE_TOPC:def_4;
then reconsider FrW = Fr W as Subset of T by XBOOLE_1:1;
A7: ( A \ {p} c= A & not p in A \ {p} ) by XBOOLE_1:36, ZFMISC_1:56;
A8: [#] (T | A) = A by PRE_TOPC:def_5;
then  p in A by A5;
then A9: A \ {p} c< A by A7, XBOOLE_0:def_8;
 (Cl W) \ W c= A \ W by A8, XBOOLE_1:33;
then  card (Fr W) <= card (A \ {p}) by A6, NAT_1:43, XBOOLE_1:1;
then  card (Fr W) < n + 1 by A4, A9, CARD_2:48, XXREAL_0:2;
then A10: card (Fr W) <= n by NAT_1:13;
then A11: Fr W in (Seq_of_ind (T | A)) . (card (Fr W)) by A2;
 n in NAT by ORDINAL1:def_12;
then  (Seq_of_ind (T | A)) . (card (Fr W)) c= (Seq_of_ind (T | A)) . n by A10, PROB_1:def_5;
then  FrW in (Seq_of_ind T) . n by A11, Th3;
hence  Fr W in (Seq_of_ind T) . n ; ::_thesis: verum
end;
then  A in (Seq_of_ind T) . (card A) by A4, Def1;
hence  ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) by Def2; ::_thesis: verum
end;
end;
end;
A12: S1[ 0 ]
proof
let T be TopSpace; ::_thesis: for A being finite Subset of T st card A <= 0 holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )
let A be finite Subset of T; ::_thesis: ( card A <= 0 implies ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) )
A13: (Seq_of_ind T) . 0 = {({} T)} by Def1;
assume A14: card A <= 0 ; ::_thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )
then  A = {} ;
then  A in {({} T)} by TARSKI:def_1;
hence  ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) by A13, A14, Def2; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A12, A1);
then  S1[ card A] ;
hence  ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) ; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster finite  ->  finite-ind for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is finite holds
b1 is finite-ind by Lm1;
cluster empty  ->  finite-ind for Element of bool (bool the carrier of T);
coherence
 for b1 being Subset-Family of T st b1 is empty holds
b1 is finite-ind
proof
let G be Subset-Family of T; ::_thesis: ( G is empty implies G is finite-ind )
assume  G is empty ; ::_thesis: G is finite-ind
then A1: G c= {({} T)} by XBOOLE_1:2;
 (Seq_of_ind T) . 0 = {({} T)} by Def1;
hence  G is finite-ind by A1, Def3; ::_thesis: verum
end;
cluster non empty finite-ind for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( not b1 is empty & b1 is finite-ind )
proof
 (Seq_of_ind T) . 0 = {({} T)} by Def1;
then  {({} T)} is finite-ind by Def3;
hence  ex b1 being Subset-Family of T st
( not b1 is empty & b1 is finite-ind ) ; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
cluster non empty finite-ind for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st
( not b1 is empty & b1 is finite-ind )
proof
consider x being set  such that
A1: x in [#] T by XBOOLE_0:def_1;
 {x} is Subset of T by A1, ZFMISC_1:31;
hence  ex b1 being Subset of T st
( not b1 is empty & b1 is finite-ind ) ; ::_thesis: verum
end;
end;

definition
let T be TopSpace;
attrT is with_finite_small_inductive_dimension  means :Def4: :: TOPDIM_1:def 4
 [#] T is with_finite_small_inductive_dimension ;
end;

:: deftheorem Def4 defines with_finite_small_inductive_dimension TOPDIM_1:def_4_:_
 for T being TopSpace holds
( T is with_finite_small_inductive_dimension iff [#] T is with_finite_small_inductive_dimension );

notation
let T be TopSpace;
synonym  finite-ind T for  with_finite_small_inductive_dimension ;
end;

registration
cluster empty TopSpace-like  ->  finite-ind for TopStruct ;
coherence
 for b1 being TopSpace st b1 is empty holds
b1 is finite-ind
proof
let T be TopSpace; ::_thesis: ( T is empty implies T is finite-ind )
assume  T is empty ; ::_thesis: T is finite-ind
then  [#] T is finite-ind ;
hence  T is finite-ind by Def4; ::_thesis: verum
end;
end;

Lm2:  for X being set holds X in (Seq_of_ind (1TopSp X)) . 1
proof
let X be set ; ::_thesis: X in (Seq_of_ind (1TopSp X)) . 1
set T = 1TopSp X;
set CT = [#] (1TopSp X);
now__::_thesis:_for_p_being_Point_of_((1TopSp_X)_|_([#]_(1TopSp_X)))
for_U_being_open_Subset_of_((1TopSp_X)_|_([#]_(1TopSp_X)))_st_p_in_U_holds_
ex_W_being_open_Subset_of_((1TopSp_X)_|_([#]_(1TopSp_X)))_st_
(_p_in_W_&_W_c=_U_&_Fr_W_in_(Seq_of_ind_(1TopSp_X))_._0_)
let p be Point of ((1TopSp X) | ([#] (1TopSp X))); ::_thesis: for U being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st p in U holds
ex W being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st
( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 )
let U be open Subset of ((1TopSp X) | ([#] (1TopSp X))); ::_thesis: ( p in U implies ex W being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st
( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 ) )
assume A1: p in U ; ::_thesis: ex W being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st
( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 )
take W = U; ::_thesis: ( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 )
A2: [#] ((1TopSp X) | ([#] (1TopSp X))) = [#] (1TopSp X) by PRE_TOPC:def_5;
then reconsider W9 = U as Subset of (1TopSp X) ;
 W9 ` is open by PRE_TOPC:def_2;
then  ( W9 is open & W9 is closed ) by PRE_TOPC:def_2, TOPS_1:3;
then  Fr W9 = {} (1TopSp X) by TOPGEN_1:14;
then A3: (Fr W9) /\ ([#] (1TopSp X)) = {} ;
 W = W /\ ([#] (1TopSp X)) by A2, XBOOLE_1:28;
then  Fr W c= {} (1TopSp X) by A3, Th1;
then A4: Fr W = {} (1TopSp X) ;
 (Seq_of_ind (1TopSp X)) . 0 = {({} (1TopSp X))} by Def1;
hence  ( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 ) by A1, A4, TARSKI:def_1; ::_thesis: verum
end;
then  [#] (1TopSp X) in (Seq_of_ind (1TopSp X)) . (0 + 1) by Def1;
hence  X in (Seq_of_ind (1TopSp X)) . 1 ; ::_thesis: verum
end;

registration
let X be set ;
cluster 1TopSp X ->  finite-ind ;
coherence
 1TopSp X is with_finite_small_inductive_dimension
proof
set T = 1TopSp X;
 [#] (1TopSp X) in (Seq_of_ind (1TopSp X)) . 1 by Lm2;
then  [#] (1TopSp X) is finite-ind by Def2;
hence  1TopSp X is with_finite_small_inductive_dimension by Def4; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like finite-ind for TopStruct ;
existence
 ex b1 being TopSpace st
( not b1 is empty & b1 is finite-ind )
proof
take  1TopSp the non empty set ; ::_thesis: ( not 1TopSp the non empty set is empty & 1TopSp the non empty set is finite-ind )
thus  ( not 1TopSp the non empty set is empty & 1TopSp the non empty set is finite-ind ) ; ::_thesis: verum
end;
end;

  begin

definition
let T be TopSpace;
let A be Subset of T;
assume B1: A is finite-ind ;
func ind A ->  Integer means :Def5: :: TOPDIM_1:def 5
( A in (Seq_of_ind T) . (it + 1) & not A in (Seq_of_ind T) . it );
existence
 ex b1 being Integer st
( A in (Seq_of_ind T) . (b1 + 1) & not A in (Seq_of_ind T) . b1 )
proof
defpred S1[ Nat] means A in (Seq_of_ind T) . $1;
A1: ex n being Nat st S1[n] by B1, Def2;
consider MIN being Nat such that
A2: S1[MIN] and
A3: for n being Nat st S1[n] holds
MIN <= n from NAT_1:sch_5(A1);
take I = MIN - 1; ::_thesis: ( A in (Seq_of_ind T) . (I + 1) & not A in (Seq_of_ind T) . I )
now__::_thesis:_not_A_in_(Seq_of_ind_T)_._I
assume A4: A in (Seq_of_ind T) . I ; ::_thesis: contradiction
then  I in dom (Seq_of_ind T) by FUNCT_1:def_2;
then reconsider i = I as Element of NAT ;
 MIN <= i by A3, A4;
then  MIN < i + 1 by NAT_1:13;
hence  contradiction ; ::_thesis: verum
end;
hence  ( A in (Seq_of_ind T) . (I + 1) & not A in (Seq_of_ind T) . I ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Integer st A in (Seq_of_ind T) . (b1 + 1) & not A in (Seq_of_ind T) . b1 & A in (Seq_of_ind T) . (b2 + 1) & not A in (Seq_of_ind T) . b2 holds
b1 = b2
proof
let I1, I2 be Integer; ::_thesis: ( A in (Seq_of_ind T) . (I1 + 1) & not A in (Seq_of_ind T) . I1 & A in (Seq_of_ind T) . (I2 + 1) & not A in (Seq_of_ind T) . I2 implies I1 = I2 )
assume that
A5: A in (Seq_of_ind T) . (I1 + 1) and
A6: not A in (Seq_of_ind T) . I1 and
A7: A in (Seq_of_ind T) . (I2 + 1) and
A8: not A in (Seq_of_ind T) . I2 ; ::_thesis: I1 = I2
 ( I1 + 1 in dom (Seq_of_ind T) & I2 + 1 in dom (Seq_of_ind T) ) by A5, A7, FUNCT_1:def_2;
then reconsider i11 = I1 + 1, i21 = I2 + 1 as Element of NAT ;
A9: I1 <= I2
proof
assume  I1 > I2 ; ::_thesis: contradiction
then A10: I1 >= i21 by INT_1:7;
then reconsider i1 = I1 as Element of NAT by INT_1:3;
 (Seq_of_ind T) . i21 c= (Seq_of_ind T) . i1 by A10, PROB_1:def_5;
hence  contradiction by A6, A7; ::_thesis: verum
end;
 I2 <= I1
proof
assume  I1 < I2 ; ::_thesis: contradiction
then A11: I2 >= i11 by INT_1:7;
then reconsider i2 = I2 as Element of NAT by INT_1:3;
 (Seq_of_ind T) . i11 c= (Seq_of_ind T) . i2 by A11, PROB_1:def_5;
hence  contradiction by A5, A8; ::_thesis: verum
end;
hence  I1 = I2 by A9, XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines ind TOPDIM_1:def_5_:_
 for T being TopSpace
for A being Subset of T st A is finite-ind holds
for b3 being Integer holds
( b3 = ind A iff ( A in (Seq_of_ind T) . (b3 + 1) & not A in (Seq_of_ind T) . b3 ) );

theorem Th5: :: TOPDIM_1:5
for T being TopSpace
for Af being finite-ind Subset of T holds - 1 <= ind Af
proof
let T be TopSpace; ::_thesis: for Af being finite-ind Subset of T holds - 1 <= ind Af
let Af be finite-ind Subset of T; ::_thesis: - 1 <= ind Af
 Af in (Seq_of_ind T) . (1 + (ind Af)) by Def5;
then A1: (ind Af) + 1 in dom (Seq_of_ind T) by FUNCT_1:def_2;
 0 = (- 1) + 1 ;
hence  - 1 <= ind Af by A1, XREAL_1:6; ::_thesis: verum
end;

theorem Th6: :: TOPDIM_1:6
for T being TopSpace
for Af being finite-ind Subset of T holds
( ind Af = - 1 iff Af is empty )
proof
let T be TopSpace; ::_thesis: for Af being finite-ind Subset of T holds
( ind Af = - 1 iff Af is empty )
let Af be finite-ind Subset of T; ::_thesis: ( ind Af = - 1 iff Af is empty )
 not - 1 in dom (Seq_of_ind T) ;
then A1: not Af in (Seq_of_ind T) . (- 1) by FUNCT_1:def_2;
A2: (Seq_of_ind T) . 0 = {({} T)} by Def1;
hereby  ::_thesis: ( Af is empty implies ind Af = - 1 )
assume  ind Af = - 1 ; ::_thesis: Af is empty
then  Af in (Seq_of_ind T) . ((- 1) + 1) by Def5;
hence  Af is empty by A2, TARSKI:def_1; ::_thesis: verum
end;
assume  Af is empty ; ::_thesis: ind Af = - 1
then A3: Af in (Seq_of_ind T) . 0 by A2, TARSKI:def_1;
 (- 1) + 1 = 0 ;
hence  ind Af = - 1 by A1, A3, Def5; ::_thesis: verum
end;

Lm3:  for T being TopSpace
for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
proof
let T be TopSpace; ::_thesis: for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
let Af be finite-ind Subset of T; ::_thesis: (ind Af) + 1 is Nat
 Af in (Seq_of_ind T) . (1 + (ind Af)) by Def5;
then  (ind Af) + 1 in dom (Seq_of_ind T) by FUNCT_1:def_2;
hence  (ind Af) + 1 is Nat ; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
let A be non empty finite-ind Subset of T;
cluster ind A ->  natural ;
coherence
 ind A is natural
proof
 ind A >= - 1 by Th5;
then  ( ind A > - 1 or ind A = - 1 ) by XXREAL_0:1;
then  ind A >= (- 1) + 1 by Th6, INT_1:7;
then  ind A in NAT by INT_1:3;
hence  ind A is natural ; ::_thesis: verum
end;
end;

theorem Th7: :: TOPDIM_1:7
for T being TopSpace
for n being Nat
for Af being finite-ind Subset of T holds
( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )
proof
let T be TopSpace; ::_thesis: for n being Nat
for Af being finite-ind Subset of T holds
( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )
let n be Nat; ::_thesis: for Af being finite-ind Subset of T holds
( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )
let Af be finite-ind Subset of T; ::_thesis: ( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )
set I = ind Af;
A1: Af in (Seq_of_ind T) . ((ind Af) + 1) by Def5;
A2: (ind Af) + 1 is Nat by Lm3;
hereby  ::_thesis: ( Af in (Seq_of_ind T) . n implies ind Af <= n - 1 )
assume  ind Af <= n - 1 ; ::_thesis: Af in (Seq_of_ind T) . n
then A3: (ind Af) + 1 <= (n - 1) + 1 by XREAL_1:6;
 ( (ind Af) + 1 in NAT & n in NAT ) by A2, ORDINAL1:def_12;
then  (Seq_of_ind T) . ((ind Af) + 1) c= (Seq_of_ind T) . n by A3, PROB_1:def_5;
hence  Af in (Seq_of_ind T) . n by A1; ::_thesis: verum
end;
assume A4: Af in (Seq_of_ind T) . n ; ::_thesis: ind Af <= n - 1
assume  ind Af > n - 1 ; ::_thesis: contradiction
then A5: ind Af >= (n - 1) + 1 by INT_1:7;
then  ( n in NAT & ind Af in NAT ) by INT_1:3;
then  (Seq_of_ind T) . n c= (Seq_of_ind T) . (ind Af) by A5, PROB_1:def_5;
hence  contradiction by A4, Def5; ::_thesis: verum
end;

theorem :: TOPDIM_1:8
for T being TopSpace
for A being finite Subset of T holds ind A < card A
proof
let T be TopSpace; ::_thesis: for A being finite Subset of T holds ind A < card A
let A be finite Subset of T; ::_thesis: ind A < card A
 A in (Seq_of_ind T) . (card A) by Lm1;
then A1: ind A <= (card A) - 1 by Th7;
 (card A) - 1 < (card A) - 0 by XREAL_1:15;
hence  ind A < card A by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th9: :: TOPDIM_1:9
for T being TopSpace
for n being Nat
for Af being finite-ind Subset of T holds
( ind Af <= n iff for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
proof
let T be TopSpace; ::_thesis: for n being Nat
for Af being finite-ind Subset of T holds
( ind Af <= n iff for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
let n be Nat; ::_thesis: for Af being finite-ind Subset of T holds
( ind Af <= n iff for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
let Af be finite-ind Subset of T; ::_thesis: ( ind Af <= n iff for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
set I = ind Af;
A1: [#] (T | Af) c= [#] T by PRE_TOPC:def_4;
A2: ( Af in (Seq_of_ind T) . ((ind Af) + 1) & not Af in (Seq_of_ind T) . (ind Af) ) by Def5;
hereby  ::_thesis: ( ( for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) ) implies ind Af <= n )
assume A3: ind Af <= n ; ::_thesis: for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
let p be Point of (T | Af); ::_thesis: for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
let U be open Subset of (T | Af); ::_thesis: ( p in U implies ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
assume A4: p in U ; ::_thesis: ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
 ( not Af is empty & not T is empty ) by A4;
then reconsider I = ind Af as Nat ;
A5: I - 1 <= n - 1 by A3, XREAL_1:9;
consider W being open Subset of (T | Af) such that
A6: ( p in W & W c= U ) and
A7: Fr W in (Seq_of_ind T) . I by A2, A4, Def1;
take W = W; ::_thesis: ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
A8: Fr W in (Seq_of_ind (T | Af)) . I by A7, Th3;
then  Fr W is finite-ind by Def2;
then  ind (Fr W) <= I - 1 by A8, Th7;
hence  ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A5, A6, A8, Def2, XXREAL_0:2; ::_thesis: verum
end;
assume A9: for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) ; ::_thesis: ind Af <= n
now__::_thesis:_for_p_being_Point_of_(T_|_Af)
for_U_being_open_Subset_of_(T_|_Af)_st_p_in_U_holds_
ex_W_being_open_Subset_of_(T_|_Af)_st_
(_p_in_W_&_W_c=_U_&_Fr_W_in_(Seq_of_ind_T)_._n_)
let p be Point of (T | Af); ::_thesis: for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
let U be open Subset of (T | Af); ::_thesis: ( p in U implies ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) )
assume  p in U ; ::_thesis: ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
then consider W being open Subset of (T | Af) such that
A10: ( p in W & W c= U ) and
A11: ( Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A9;
A12: Fr W is Subset of T by A1, XBOOLE_1:1;
 Fr W in (Seq_of_ind (T | Af)) . n by A11, Th7;
then  Fr W in (Seq_of_ind T) . n by A12, Th3;
hence  ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) by A10; ::_thesis: verum
end;
then  Af in (Seq_of_ind T) . (n + 1) by Def1;
then  ind Af <= (n + 1) - 1 by Th7;
hence  ind Af <= n ; ::_thesis: verum
end;

definition
let T be TopSpace;
let G be Subset-Family of T;
assume B1: G is finite-ind ;
func ind G ->  Integer means :Def6: :: TOPDIM_1:def 6
( G c= (Seq_of_ind T) . (it + 1) & - 1 <= it & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
it <= i ) );
existence
 ex b1 being Integer st
( G c= (Seq_of_ind T) . (b1 + 1) & - 1 <= b1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b1 <= i ) )
proof
defpred S1[ Nat] means G c= (Seq_of_ind T) . $1;
A1: ex n being Nat st S1[n] by B1, Def3;
consider MIN being Nat such that
A2: S1[MIN] and
A3: for n being Nat st S1[n] holds
MIN <= n from NAT_1:sch_5(A1);
take I = MIN - 1; ::_thesis: ( G c= (Seq_of_ind T) . (I + 1) & - 1 <= I & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I <= i ) )
A4: now__::_thesis:_for_i_being_Integer_st_-_1_<=_i_&_G_c=_(Seq_of_ind_T)_._(i_+_1)_holds_
I_<=_i
let i be Integer; ::_thesis: ( - 1 <= i & G c= (Seq_of_ind T) . (i + 1) implies I <= i )
assume that
A5: - 1 <= i and
A6: G c= (Seq_of_ind T) . (i + 1) ; ::_thesis: I <= i
 (- 1) + 1 <= i + 1 by A5, XREAL_1:6;
then  i + 1 in NAT by INT_1:3;
then reconsider I1 = i + 1 as Nat ;
 ( MIN = I + 1 & MIN <= I1 ) by A3, A6;
hence  I <= i by XREAL_1:6; ::_thesis: verum
end;
 I >= 0 - 1 by XREAL_1:9;
hence  ( G c= (Seq_of_ind T) . (I + 1) & - 1 <= I & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I <= i ) ) by A2, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Integer st G c= (Seq_of_ind T) . (b1 + 1) & - 1 <= b1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b1 <= i ) & G c= (Seq_of_ind T) . (b2 + 1) & - 1 <= b2 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b2 <= i ) holds
b1 = b2
proof
let I1, I2 be Integer; ::_thesis: ( G c= (Seq_of_ind T) . (I1 + 1) & - 1 <= I1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I1 <= i ) & G c= (Seq_of_ind T) . (I2 + 1) & - 1 <= I2 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I2 <= i ) implies I1 = I2 )
assume  ( G c= (Seq_of_ind T) . (I1 + 1) & - 1 <= I1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I1 <= i ) & G c= (Seq_of_ind T) . (I2 + 1) & - 1 <= I2 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I2 <= i ) ) ; ::_thesis: I1 = I2
then  ( I2 <= I1 & I1 <= I2 ) ;
hence  I1 = I2 by XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines ind TOPDIM_1:def_6_:_
 for T being TopSpace
for G being Subset-Family of T st G is finite-ind holds
for b3 being Integer holds
( b3 = ind G iff ( G c= (Seq_of_ind T) . (b3 + 1) & - 1 <= b3 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b3 <= i ) ) );

theorem :: TOPDIM_1:10
for T being TopSpace
for G being Subset-Family of T holds
( ( ind G = - 1 & G is finite-ind ) iff G c= {({} T)} )
proof
let T be TopSpace; ::_thesis: for G being Subset-Family of T holds
( ( ind G = - 1 & G is finite-ind ) iff G c= {({} T)} )
let G be Subset-Family of T; ::_thesis: ( ( ind G = - 1 & G is finite-ind ) iff G c= {({} T)} )
A1: {({} T)} = (Seq_of_ind T) . 0 by Def1;
 0 = (- 1) + 1 ;
hence  ( ind G = - 1 & G is finite-ind implies G c= {({} T)} ) by A1, Def6; ::_thesis: ( G c= {({} T)} implies ( ind G = - 1 & G is finite-ind ) )
assume A2: G c= {({} T)} ; ::_thesis: ( ind G = - 1 & G is finite-ind )
then A3: G is finite-ind by A1, Def3;
then A4: - 1 <= ind G by Def6;
 0 = (- 1) + 1 ;
then  ind G <= - 1 by A1, A2, A3, Def6;
hence  ( ind G = - 1 & G is finite-ind ) by A1, A2, A4, Def3, XXREAL_0:1; ::_thesis: verum
end;

theorem Th11: :: TOPDIM_1:11
for T being TopSpace
for G being Subset-Family of T
for I being Integer holds
( G is finite-ind & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ) ) )
proof
let T be TopSpace; ::_thesis: for G being Subset-Family of T
for I being Integer holds
( G is finite-ind & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ) ) )
let G be Subset-Family of T; ::_thesis: for I being Integer holds
( G is finite-ind & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ) ) )
let I be Integer; ::_thesis: ( G is finite-ind & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ) ) )
hereby  ::_thesis: ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ) implies ( G is finite-ind & ind G <= I ) )
assume that
A1: G is finite-ind and
A2: ind G <= I ; ::_thesis: ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ) )
 ind G >= - 1 by A1, Def6;
then  (ind G) + 1 >= (- 1) + 1 by XREAL_1:6;
then  (ind G) + 1 in NAT by INT_1:3;
then reconsider iG = (ind G) + 1 as Nat ;
A3: G c= (Seq_of_ind T) . iG by A1, Def6;
 - 1 <= ind G by A1, Def6;
hence  - 1 <= I by A2, XXREAL_0:2; ::_thesis: for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I )
let A be Subset of T; ::_thesis: ( A in G implies ( A is finite-ind & ind A <= I ) )
assume A4: A in G ; ::_thesis: ( A is finite-ind & ind A <= I )
thus  A is finite-ind by A1, A4, Th4; ::_thesis: ind A <= I
then  ind A <= iG - 1 by A3, A4, Th7;
hence  ind A <= I by A2, XXREAL_0:2; ::_thesis: verum
end;
assume that
A5: - 1 <= I and
A6: for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ; ::_thesis: ( G is finite-ind & ind G <= I )
 (- 1) + 1 <= I + 1 by A5, XREAL_1:6;
then reconsider I1 = I + 1 as Element of NAT by INT_1:3;
A7: G c= (Seq_of_ind T) . I1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G or x in (Seq_of_ind T) . I1 )
assume A8: x in G ; ::_thesis: x in (Seq_of_ind T) . I1
reconsider A = x as Subset of T by A8;
A9: I = I1 - 1 ;
 ( A is finite-ind & ind A <= I ) by A6, A8;
hence  x in (Seq_of_ind T) . I1 by A9, Th7; ::_thesis: verum
end;
then  G is finite-ind by Def3;
hence  ( G is finite-ind & ind G <= I ) by A5, A7, Def6; ::_thesis: verum
end;

theorem :: TOPDIM_1:12
for T being TopSpace
for G1, G2 being Subset-Family of T st G1 is finite-ind & G2 c= G1 holds
( G2 is finite-ind & ind G2 <= ind G1 )
proof
let T be TopSpace; ::_thesis: for G1, G2 being Subset-Family of T st G1 is finite-ind & G2 c= G1 holds
( G2 is finite-ind & ind G2 <= ind G1 )
let G1, G2 be Subset-Family of T; ::_thesis: ( G1 is finite-ind & G2 c= G1 implies ( G2 is finite-ind & ind G2 <= ind G1 ) )
assume that
A1: G1 is finite-ind and
A2: G2 c= G1 ; ::_thesis: ( G2 is finite-ind & ind G2 <= ind G1 )
A3: - 1 <= ind G1 by A1, Th11;
then  for A being Subset of T st A in G2 holds
( A is finite-ind & ind A <= ind G1 ) by A1, A2, Th11;
hence  ( G2 is finite-ind & ind G2 <= ind G1 ) by A3, Th11; ::_thesis: verum
end;

Lm4:  for T being TopSpace
for G, G1 being Subset-Family of T
for i being Integer st G is finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i holds
( G \/ G1 is finite-ind & ind (G \/ G1) <= i )
proof
let T be TopSpace; ::_thesis: for G, G1 being Subset-Family of T
for i being Integer st G is finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i holds
( G \/ G1 is finite-ind & ind (G \/ G1) <= i )
let G, G1 be Subset-Family of T; ::_thesis: for i being Integer st G is finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i holds
( G \/ G1 is finite-ind & ind (G \/ G1) <= i )
let i be Integer; ::_thesis: ( G is finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i implies ( G \/ G1 is finite-ind & ind (G \/ G1) <= i ) )
assume that
A1: G is finite-ind and
A2: G1 is finite-ind and
A3: ind G <= i and
A4: ind G1 <= i ; ::_thesis: ( G \/ G1 is finite-ind & ind (G \/ G1) <= i )
A5: for A being Subset of T st A in G \/ G1 holds
( A is finite-ind & ind A <= i )
proof
let A be Subset of T; ::_thesis: ( A in G \/ G1 implies ( A is finite-ind & ind A <= i ) )
assume  A in G \/ G1 ; ::_thesis: ( A is finite-ind & ind A <= i )
then  ( A in G or A in G1 ) by XBOOLE_0:def_3;
hence  ( A is finite-ind & ind A <= i ) by A1, A2, A3, A4, Th11; ::_thesis: verum
end;
 - 1 <= i by A1, A3, Th11;
hence  ( G \/ G1 is finite-ind & ind (G \/ G1) <= i ) by A5, Th11; ::_thesis: verum
end;

registration
let T be TopSpace;
let G1, G2 be finite-ind Subset-Family of T;
clusterG1 \/ G2 ->  finite-ind for Subset-Family of T;
coherence
 for b1 being Subset-Family of T st b1 = G1 \/ G2 holds
b1 is with_finite_small_inductive_dimension
proof
set iG1 = (ind G1) + 1;
set iG2 = (ind G2) + 1;
 - 1 <= ind G1 by Def6;
then  (- 1) + 1 <= (ind G1) + 1 by XREAL_1:6;
then A1: (ind G1) + 1 in NAT by INT_1:3;
 - 1 <= ind G2 by Def6;
then  (- 1) + 1 <= (ind G2) + 1 by XREAL_1:6;
then A2: (ind G2) + 1 in NAT by INT_1:3;
then  ( (ind G1) + 0 <= (ind G1) + 1 & (ind G1) + 1 <= ((ind G1) + 1) + ((ind G2) + 1) ) by A1, NAT_1:11, XREAL_1:6;
then A3: ind G1 <= ((ind G1) + 1) + ((ind G2) + 1) by XXREAL_0:2;
 ( (ind G2) + 0 <= (ind G2) + 1 & (ind G2) + 1 <= ((ind G2) + 1) + ((ind G1) + 1) ) by A2, A1, NAT_1:11, XREAL_1:6;
then  ind G2 <= ((ind G1) + 1) + ((ind G2) + 1) by XXREAL_0:2;
hence  for b1 being Subset-Family of T st b1 = G1 \/ G2 holds
b1 is with_finite_small_inductive_dimension by A3, Lm4; ::_thesis: verum
end;
end;

theorem :: TOPDIM_1:13
for T being TopSpace
for G, G1 being Subset-Family of T
for I being Integer st G is finite-ind & G1 is finite-ind & ind G <= I & ind G1 <= I holds
ind (G \/ G1) <= I by Lm4;

definition
let T be TopSpace;
func ind T ->  Integer equals :: TOPDIM_1:def 7
 ind ([#] T);
correctness
coherence
ind ([#] T) is Integer;
;
end;

:: deftheorem  defines ind TOPDIM_1:def_7_:_
 for T being TopSpace holds ind T = ind ([#] T);

registration
let T be non empty finite-ind TopSpace;
cluster ind T ->  natural ;
coherence
 ind T is natural
proof
 ( not [#] T is empty & [#] T is finite-ind ) by Def4;
hence  ind T is natural ; ::_thesis: verum
end;
end;

theorem :: TOPDIM_1:14
for X being non empty set holds ind (1TopSp X) = 0
proof
let X be non empty set ; ::_thesis: ind (1TopSp X) = 0
set T = 1TopSp X;
 (Seq_of_ind (1TopSp X)) . 0 = {({} (1TopSp X))} by Def1;
then A1: not [#] (1TopSp X) in (Seq_of_ind (1TopSp X)) . 0 by TARSKI:def_1;
A2: [#] (1TopSp X) in (Seq_of_ind (1TopSp X)) . (0 + 1) by Lm2;
then  [#] (1TopSp X) is finite-ind by Def2;
hence  ind (1TopSp X) = 0 by A1, A2, Def5; ::_thesis: verum
end;

theorem Th15: :: TOPDIM_1:15
for T being TopSpace st ex n being Nat st
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 ) holds
T is finite-ind
proof
let T be TopSpace; ::_thesis: ( ex n being Nat st
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 ) implies T is finite-ind )
given n being Nat such that A1: 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 ) ; ::_thesis: T is finite-ind
set CT = [#] T;
set TT = T | ([#] T);
A2: [#] (T | ([#] T)) = [#] T by PRE_TOPC:def_5;
 T is SubSpace of T by TSEP_1:2;
then A3: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (T | ([#] T)), the topology of (T | ([#] T)) #) by A2, TSEP_1:5;
now__::_thesis:_for_p9_being_Point_of_(T_|_([#]_T))
for_U9_being_open_Subset_of_(T_|_([#]_T))_st_p9_in_U9_holds_
ex_W9_being_open_Subset_of_(T_|_([#]_T))_st_
(_p9_in_W9_&_W9_c=_U9_&_Fr_W9_in_(Seq_of_ind_T)_._n_)
let p9 be Point of (T | ([#] T)); ::_thesis: for U9 being open Subset of (T | ([#] T)) st p9 in U9 holds
ex W9 being open Subset of (T | ([#] T)) st
( p9 in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind T) . n )
let U9 be open Subset of (T | ([#] T)); ::_thesis: ( p9 in U9 implies ex W9 being open Subset of (T | ([#] T)) st
( p9 in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind T) . n ) )
assume A4: p9 in U9 ; ::_thesis: ex W9 being open Subset of (T | ([#] T)) st
( p9 in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind T) . n )
reconsider p = p9 as Point of T by A2;
 U9 in the topology of (T | ([#] T)) by PRE_TOPC:def_2;
then reconsider U = U9 as open Subset of T by A3, PRE_TOPC:def_2;
consider W being open Subset of T such that
A5: p in W and
A6: ( W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A1, A4;
 W in the topology of T by PRE_TOPC:def_2;
then reconsider W9 = W as open Subset of (T | ([#] T)) by A3, PRE_TOPC:def_2;
take W9 = W9; ::_thesis: ( p9 in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind T) . n )
 not T is empty by A5;
then  ( Cl W = Cl W9 & Int W = Int W9 ) by A2, TOPS_3:54;
then  Fr W = (Cl W9) \ (Int W9) by TOPGEN_1:8
.= Fr W9 by TOPGEN_1:8 ;
hence  ( p9 in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind T) . n ) by A5, A6, Th7; ::_thesis: verum
end;
then  [#] T in (Seq_of_ind T) . (n + 1) by Def1;
then  [#] T is finite-ind by Def2;
hence  T is finite-ind by Def4; ::_thesis: verum
end;

theorem Th16: :: TOPDIM_1:16
for n being Nat
for Tf being finite-ind TopSpace holds
( ind Tf <= n iff for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
proof
let n be Nat; ::_thesis: for Tf being finite-ind TopSpace holds
( ind Tf <= n iff for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
let Tf be finite-ind TopSpace; ::_thesis: ( ind Tf <= n iff for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
set CT = [#] Tf;
set TT = Tf | ([#] Tf);
A1: [#] (Tf | ([#] Tf)) = [#] Tf by PRE_TOPC:def_5;
 Tf is SubSpace of Tf by TSEP_1:2;
then A2: TopStruct(# the carrier of Tf, the topology of Tf #) = TopStruct(# the carrier of (Tf | ([#] Tf)), the topology of (Tf | ([#] Tf)) #) by A1, TSEP_1:5;
A3: [#] Tf is finite-ind by Def4;
hereby  ::_thesis: ( ( for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) ) implies ind Tf <= n )
assume A4: ind Tf <= n ; ::_thesis: for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
let p be Point of Tf; ::_thesis: for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
let U be open Subset of Tf; ::_thesis: ( p in U implies ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
assume A5: p in U ; ::_thesis: ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
reconsider p9 = p as Point of (Tf | ([#] Tf)) by A1;
 U in the topology of Tf by PRE_TOPC:def_2;
then reconsider U9 = U as open Subset of (Tf | ([#] Tf)) by A2, PRE_TOPC:def_2;
consider W9 being open Subset of (Tf | ([#] Tf)) such that
A6: ( p9 in W9 & W9 c= U9 ) and
A7: ( Fr W9 is finite-ind & ind (Fr W9) <= n - 1 ) by A3, A4, A5, Th9;
 W9 in the topology of (Tf | ([#] Tf)) by PRE_TOPC:def_2;
then reconsider W = W9 as open Subset of Tf by A2, PRE_TOPC:def_2;
 not Tf is empty by A5;
then  ( Cl W = Cl W9 & Int W = Int W9 ) by A1, TOPS_3:54;
then A8: Fr W = (Cl W9) \ (Int W9) by TOPGEN_1:8
.= Fr W9 by TOPGEN_1:8 ;
take W = W; ::_thesis: ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
 Fr W9 in (Seq_of_ind (Tf | ([#] Tf))) . n by A7, Th7;
then A9: Fr W in (Seq_of_ind Tf) . n by A8, Th3;
then  Fr W is finite-ind by Def2;
hence  ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A6, A9, Th7; ::_thesis: verum
end;
assume A10: for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) ; ::_thesis: ind Tf <= n
now__::_thesis:_for_p9_being_Point_of_(Tf_|_([#]_Tf))
for_U9_being_open_Subset_of_(Tf_|_([#]_Tf))_st_p9_in_U9_holds_
ex_W9_being_open_Subset_of_(Tf_|_([#]_Tf))_st_
(_p9_in_W9_&_W9_c=_U9_&_Fr_W9_is_finite-ind_&_ind_(Fr_W9)_<=_n_-_1_)
let p9 be Point of (Tf | ([#] Tf)); ::_thesis: for U9 being open Subset of (Tf | ([#] Tf)) st p9 in U9 holds
ex W9 being open Subset of (Tf | ([#] Tf)) st
( p9 in W9 & W9 c= U9 & Fr W9 is finite-ind & ind (Fr W9) <= n - 1 )
let U9 be open Subset of (Tf | ([#] Tf)); ::_thesis: ( p9 in U9 implies ex W9 being open Subset of (Tf | ([#] Tf)) st
( p9 in W9 & W9 c= U9 & Fr W9 is finite-ind & ind (Fr W9) <= n - 1 ) )
assume A11: p9 in U9 ; ::_thesis: ex W9 being open Subset of (Tf | ([#] Tf)) st
( p9 in W9 & W9 c= U9 & Fr W9 is finite-ind & ind (Fr W9) <= n - 1 )
reconsider p = p9 as Point of Tf by A1;
 U9 in the topology of (Tf | ([#] Tf)) by PRE_TOPC:def_2;
then reconsider U = U9 as open Subset of Tf by A2, PRE_TOPC:def_2;
consider W being open Subset of Tf such that
A12: ( p in W & W c= U ) and
A13: ( Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A10, A11;
 W in the topology of Tf by PRE_TOPC:def_2;
then reconsider W9 = W as open Subset of (Tf | ([#] Tf)) by A2, PRE_TOPC:def_2;
 not Tf is empty by A11;
then  ( Cl W = Cl W9 & Int W = Int W9 ) by A1, TOPS_3:54;
then A14: Fr W = (Cl W9) \ (Int W9) by TOPGEN_1:8
.= Fr W9 by TOPGEN_1:8 ;
take W9 = W9; ::_thesis: ( p9 in W9 & W9 c= U9 & Fr W9 is finite-ind & ind (Fr W9) <= n - 1 )
 Fr W in (Seq_of_ind Tf) . n by A13, Th7;
then A15: Fr W9 in (Seq_of_ind (Tf | ([#] Tf))) . n by A14, Th3;
then  Fr W9 is finite-ind by Def2;
hence  ( p9 in W9 & W9 c= U9 & Fr W9 is finite-ind & ind (Fr W9) <= n - 1 ) by A12, A15, Th7; ::_thesis: verum
end;
hence  ind Tf <= n by A3, Th9; ::_thesis: verum
end;

Lm5:  for T being TopSpace
for Af being finite-ind Subset of T holds
( T | Af is finite-ind & ind (T | Af) = ind Af )
proof
let T be TopSpace; ::_thesis: for Af being finite-ind Subset of T holds
( T | Af is finite-ind & ind (T | Af) = ind Af )
let Af be finite-ind Subset of T; ::_thesis: ( T | Af is finite-ind & ind (T | Af) = ind Af )
set TA = T | Af;
A1: [#] (T | Af) = Af by PRE_TOPC:def_5;
percases ( ind Af = - 1 or not Af is empty ) by Th6;
supposeA2: ind Af = - 1 ; ::_thesis: ( T | Af is finite-ind & ind (T | Af) = ind Af )
then  Af = {} T by Th6;
hence  ( T | Af is finite-ind & ind (T | Af) = ind Af ) by A2, Th6; ::_thesis: verum
end;
supposeA3: not Af is empty ; ::_thesis: ( T | Af is finite-ind & ind (T | Af) = ind Af )
then  not T is empty ;
then reconsider n = ind Af as Nat by A3;
 Af in (Seq_of_ind T) . (n + 1) by Def5;
then A4: [#] (T | Af) in (Seq_of_ind (T | Af)) . (n + 1) by A1, Th3;
then A5: [#] (T | Af) is finite-ind by Def2;
hence  T | Af is finite-ind by Def4; ::_thesis: ind (T | Af) = ind Af
A6: ind ([#] (T | Af)) >= n
proof
assume  ind ([#] (T | Af)) < n ; ::_thesis: contradiction
then  (ind ([#] (T | Af))) + 1 <= n by INT_1:7;
then  ((ind ([#] (T | Af))) + 1) - 1 <= n - 1 by XREAL_1:9;
then  [#] (T | Af) in (Seq_of_ind (T | Af)) . n by A5, Th7;
then  Af in (Seq_of_ind T) . n by A1, Th3;
hence  contradiction by Def5; ::_thesis: verum
end;
 ind ([#] (T | Af)) <= (n + 1) - 1 by A4, A5, Th7;
hence  ind (T | Af) = ind Af by A6, XXREAL_0:1; ::_thesis: verum
end;
end;
end;

Lm6:  for Tf being finite-ind TopSpace
for A being Subset of Tf holds
( Tf | A is finite-ind & ind (Tf | A) <= ind Tf )
proof
let Tf be finite-ind TopSpace; ::_thesis: for A being Subset of Tf holds
( Tf | A is finite-ind & ind (Tf | A) <= ind Tf )
defpred S1[ Nat] means  for T being TopSpace st T is finite-ind & ind T = $1 - 1 holds
for A being Subset of T holds
( T | A is finite-ind & ind (T | A) <= ind T );
 [#] Tf is finite-ind by Def4;
then reconsider i = (ind Tf) + 1 as Nat by Lm3;
A1: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
proof
let n9 be Nat; ::_thesis: ( ( for n being Nat st n < n9 holds
S1[n] ) implies S1[n9] )
assume A2: for n being Nat st n < n9 holds
S1[n] ; ::_thesis: S1[n9]
percases ( n9 = 0 or n9 > 0 ) ;
supposeA3: n9 = 0 ; ::_thesis: S1[n9]
let T be TopSpace; ::_thesis: ( T is finite-ind & ind T = n9 - 1 implies for A being Subset of T holds
( T | A is finite-ind & ind (T | A) <= ind T ) )
assume that
A4: T is finite-ind and
A5: ind T = n9 - 1 ; ::_thesis: for A being Subset of T holds
( T | A is finite-ind & ind (T | A) <= ind T )
let A be Subset of T; ::_thesis: ( T | A is finite-ind & ind (T | A) <= ind T )
 [#] T is finite-ind by A4, Def4;
then  [#] T = {} T by A3, A5, Th6;
hence  ( T | A is finite-ind & ind (T | A) <= ind T ) by A3, A5, Th6; ::_thesis: verum
end;
suppose n9 > 0 ; ::_thesis: S1[n9]
then reconsider n = n9 - 1 as Nat by NAT_1:20;
let T be TopSpace; ::_thesis: ( T is finite-ind & ind T = n9 - 1 implies for A being Subset of T holds
( T | A is finite-ind & ind (T | A) <= ind T ) )
assume that
A6: T is finite-ind and
A7: ind T = n9 - 1 ; ::_thesis: for A being Subset of T holds
( T | A is finite-ind & ind (T | A) <= ind T )
let A be Subset of T; ::_thesis: ( T | A is finite-ind & ind (T | A) <= ind T )
set TA = T | A;
A8: [#] (T | A) = A by PRE_TOPC:def_5;
A9: now__::_thesis:_for_p_being_Point_of_(T_|_A)
for_U_being_open_Subset_of_(T_|_A)_st_p_in_U_holds_
ex_W_being_open_Subset_of_(T_|_A)_st_
(_p_in_W_&_W_c=_U_&_Fr_W_is_finite-ind_&_ind_(Fr_W)_<=_n_-_1_)
let p be Point of (T | A); ::_thesis: for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
let U be open Subset of (T | A); ::_thesis: ( p in U implies ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
assume A10: p in U ; ::_thesis: ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
 U in the topology of (T | A) by PRE_TOPC:def_2;
then consider U9 being Subset of T such that
A11: U9 in the topology of T and
A12: U = U9 /\ ([#] (T | A)) by PRE_TOPC:def_4;
A13: p in U9 by A10, A12, XBOOLE_0:def_4;
then reconsider p9 = p as Point of T ;
 U9 is open Subset of T by A11, PRE_TOPC:def_2;
then consider W9 being open Subset of T such that
A14: ( p9 in W9 & W9 c= U9 ) and
A15: Fr W9 is finite-ind and
A16: ind (Fr W9) <= n - 1 by A6, A7, A13, Th16;
reconsider i = (ind (Fr W9)) + 1 as Nat by A15, Lm3;
 ((ind (Fr W9)) + 1) - 1 <= n - 1 by A16;
then  ( n9 - 1 < n9 - 0 & (ind (Fr W9)) + 1 <= n9 - 1 ) by XREAL_1:9, XREAL_1:10;
then  (ind (Fr W9)) + 1 < n9 by XXREAL_0:2;
then A17: S1[i] by A2;
reconsider W = W9 /\ ([#] (T | A)) as Subset of (T | A) ;
 W9 in the topology of T by PRE_TOPC:def_2;
then  W in the topology of (T | A) by PRE_TOPC:def_4;
then reconsider W = W as open Subset of (T | A) by PRE_TOPC:def_2;
set FR9 = Fr W9;
set TF = T | (Fr W9);
 ( [#] (T | (Fr W9)) = Fr W9 & Fr W c= (Fr W9) /\ A ) by A8, Th1, PRE_TOPC:def_5;
then reconsider FrW = Fr W as Subset of (T | (Fr W9)) by XBOOLE_1:18;
take W = W; ::_thesis: ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
 [#] (T | (Fr W9)) c= [#] T by PRE_TOPC:def_4;
then reconsider FrW9 = FrW as Subset of T by XBOOLE_1:1;
A18: ( T | (Fr W9) is finite-ind & ind (T | (Fr W9)) = ind (Fr W9) ) by A15, Lm5;
then  (T | (Fr W9)) | FrW is finite-ind by A17;
then A19: [#] ((T | (Fr W9)) | FrW) is finite-ind by Def4;
 ind ((T | (Fr W9)) | FrW) <= ind (Fr W9) by A17, A18;
then  ind ([#] ((T | (Fr W9)) | FrW)) <= n - 1 by A16, XXREAL_0:2;
then  ( [#] ((T | (Fr W9)) | FrW) = FrW & [#] ((T | (Fr W9)) | FrW) in (Seq_of_ind ((T | (Fr W9)) | FrW)) . n ) by A19, Th7, PRE_TOPC:def_5;
then  FrW in (Seq_of_ind (T | (Fr W9))) . n by Th3;
then  FrW9 in (Seq_of_ind T) . n by Th3;
then A20: Fr W in (Seq_of_ind (T | A)) . n by Th3;
then  Fr W is finite-ind by Def2;
hence  ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A10, A12, A14, A20, Th7, XBOOLE_0:def_4, XBOOLE_1:26; ::_thesis: verum
end;
then  T | A is finite-ind by Th15;
hence  ( T | A is finite-ind & ind (T | A) <= ind T ) by A7, A9, Th16; ::_thesis: verum
end;
end;
end;
 for n being Nat holds S1[n] from NAT_1:sch_4(A1);
then  S1[i] ;
hence  for A being Subset of Tf holds
( Tf | A is finite-ind & ind (Tf | A) <= ind Tf ) ; ::_thesis: verum
end;

Lm7:  for T being TopSpace
for A being Subset of T st T is finite-ind holds
A is finite-ind
proof
let T be TopSpace; ::_thesis: for A being Subset of T st T is finite-ind holds
A is finite-ind
let A be Subset of T; ::_thesis: ( T is finite-ind implies A is finite-ind )
set TA = T | A;
assume  T is finite-ind ; ::_thesis: A is finite-ind
then  T | A is finite-ind by Lm6;
then  [#] (T | A) is finite-ind by Def4;
then consider n being Nat such that
A1: [#] (T | A) in (Seq_of_ind (T | A)) . n by Def2;
 [#] (T | A) = A by PRE_TOPC:def_5;
then  A in (Seq_of_ind T) . n by A1, Th3;
hence  A is finite-ind by Def2; ::_thesis: verum
end;

begin

registration
let Tf be finite-ind TopSpace;
cluster  ->  finite-ind for Element of bool the carrier of Tf;
coherence
 for b1 being Subset of Tf holds b1 is finite-ind by Lm7;
end;

registration
let T be TopSpace;
let Af be finite-ind Subset of T;
clusterT | Af ->  finite-ind ;
coherence
 T | Af is with_finite_small_inductive_dimension by Lm5;
end;

theorem :: TOPDIM_1:17
for T being TopSpace
for Af being finite-ind Subset of T holds ind (T | Af) = ind Af by Lm5;

theorem Th18: :: TOPDIM_1:18
for T being TopSpace
for A being Subset of T st T | A is finite-ind holds
A is finite-ind
proof
let T be TopSpace; ::_thesis: for A being Subset of T st T | A is finite-ind holds
A is finite-ind
let A be Subset of T; ::_thesis: ( T | A is finite-ind implies A is finite-ind )
assume  T | A is finite-ind ; ::_thesis: A is finite-ind
then consider n being Nat such that
A1: [#] (T | A) in (Seq_of_ind (T | A)) . n by Def2;
 [#] (T | A) = A by PRE_TOPC:def_5;
then  A in (Seq_of_ind T) . n by A1, Th3;
hence  A is finite-ind by Def2; ::_thesis: verum
end;

theorem Th19: :: TOPDIM_1:19
for T being TopSpace
for A being Subset of T
for Af being finite-ind Subset of T st A c= Af holds
( A is finite-ind & ind A <= ind Af )
proof
let T be TopSpace; ::_thesis: for A being Subset of T
for Af being finite-ind Subset of T st A c= Af holds
( A is finite-ind & ind A <= ind Af )
let A be Subset of T; ::_thesis: for Af being finite-ind Subset of T st A c= Af holds
( A is finite-ind & ind A <= ind Af )
let Af be finite-ind Subset of T; ::_thesis: ( A c= Af implies ( A is finite-ind & ind A <= ind Af ) )
assume A1: A c= Af ; ::_thesis: ( A is finite-ind & ind A <= ind Af )
 [#] (T | Af) = Af by PRE_TOPC:def_5;
then reconsider A9 = A as Subset of (T | Af) by A1;
A2: ind (T | Af) = ind Af by Lm5;
A3: (T | Af) | A9 = T | A by METRIZTS:9;
hence  A is finite-ind by Th18; ::_thesis: ind A <= ind Af
then  ind (T | A) = ind A by Lm5;
hence  ind A <= ind Af by A2, A3, Lm6; ::_thesis: verum
end;

theorem :: TOPDIM_1:20
for Tf being finite-ind TopSpace
for A being Subset of Tf holds ind A <= ind Tf by Th19;

theorem Th21: :: TOPDIM_1:21
for T being TopSpace
for A, B being Subset of T
for F being Subset of (T | A) st F = B & B is finite-ind holds
( F is finite-ind & ind F = ind B )
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T
for F being Subset of (T | A) st F = B & B is finite-ind holds
( F is finite-ind & ind F = ind B )
let A, B be Subset of T; ::_thesis: for F being Subset of (T | A) st F = B & B is finite-ind holds
( F is finite-ind & ind F = ind B )
let F be Subset of (T | A); ::_thesis: ( F = B & B is finite-ind implies ( F is finite-ind & ind F = ind B ) )
assume that
A1: F = B and
A2: B is finite-ind ; ::_thesis: ( F is finite-ind & ind F = ind B )
A3: (T | A) | F = T | B by A1, METRIZTS:9;
then  F is finite-ind by A2, Th18;
then  ind F = ind ((T | A) | F) by Lm5
.= ind (T | B) by A1, METRIZTS:9
.= ind B by A2, Lm5 ;
hence  ( F is finite-ind & ind F = ind B ) by A2, A3, Th18; ::_thesis: verum
end;

theorem Th22: :: TOPDIM_1:22
for T being TopSpace
for A, B being Subset of T
for F being Subset of (T | A) st F = B & F is finite-ind holds
( B is finite-ind & ind F = ind B )
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T
for F being Subset of (T | A) st F = B & F is finite-ind holds
( B is finite-ind & ind F = ind B )
let A, B be Subset of T; ::_thesis: for F being Subset of (T | A) st F = B & F is finite-ind holds
( B is finite-ind & ind F = ind B )
let F be Subset of (T | A); ::_thesis: ( F = B & F is finite-ind implies ( B is finite-ind & ind F = ind B ) )
assume that
A1: F = B and
A2: F is finite-ind ; ::_thesis: ( B is finite-ind & ind F = ind B )
A3: (T | A) | F = T | B by A1, METRIZTS:9;
then A4: B is finite-ind by A2, Th18;
ind F = ind ((T | A) | F) by A2, Lm5
.= ind (T | B) by A1, METRIZTS:9
.= ind B by A4, Lm5 ;
hence  ( B is finite-ind & ind F = ind B ) by A2, A3, Th18; ::_thesis: verum
end;

Lm8:  for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds
( T2 is finite-ind & ind T2 <= ind T1 )
proof
defpred S1[ Nat] means  for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind & ind T1 <= $1 holds
( T2 is finite-ind & ind T2 <= ind T1 );
let T1, T2 be TopSpace; ::_thesis: ( T1,T2 are_homeomorphic & T1 is finite-ind implies ( T2 is finite-ind & ind T2 <= ind T1 ) )
assume that
A1: T1,T2 are_homeomorphic and
A2: T1 is finite-ind ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
reconsider i = (ind T1) + 1 as Nat by A2, Lm3;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
set n1 = n + 1;
let T1, T2 be TopSpace; ::_thesis: ( T1,T2 are_homeomorphic & T1 is finite-ind & ind T1 <= n + 1 implies ( T2 is finite-ind & ind T2 <= ind T1 ) )
assume that
A5: T1,T2 are_homeomorphic and
A6: T1 is finite-ind and
A7: ind T1 <= n + 1 ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
consider f being Function of T1,T2 such that
A8: f is being_homeomorphism by A5, T_0TOPSP:def_1;
set f9 = f " ;
A9: dom f = [#] T1 by A8, TOPS_2:def_5;
A10: rng f = [#] T2 by A8, TOPS_2:def_5;
A11: f is onto by A10, FUNCT_2:def_3;
A12: f is one-to-one by A8, TOPS_2:def_5;
percases ( [#] T1 = {} T1 or [#] T1 <> {} T1 ) ;
supposeA13: [#] T1 = {} T1 ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
then  ind T1 = - 1 by Th6;
hence  ( T2 is finite-ind & ind T2 <= ind T1 ) by A10, A13, Def4, Th6; ::_thesis: verum
end;
supposeA14: [#] T1 <> {} T1 ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
then  not T1 is empty ;
then reconsider i = ind T1 as Nat by A6;
A15: not T1 is empty by A14;
A16: not T2 is empty by A9, A14;
percases ( i <= n or ind T1 = n + 1 ) by A7, NAT_1:8;
suppose i <= n ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
hence  ( T2 is finite-ind & ind T2 <= ind T1 ) by A4, A5, A6; ::_thesis: verum
end;
supposeA17: ind T1 = n + 1 ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
A18: dom (f ") = [#] T2 by A10, A12, A16, TOPS_2:49;
A19: for p being Point of T2
for U being open Subset of T2 st p in U holds
ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (n + 1) - 1 )
proof
reconsider F = f as Function ;
let p be Point of T2; ::_thesis: for U being open Subset of T2 st p in U holds
ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (n + 1) - 1 )
let U be open Subset of T2; ::_thesis: ( p in U implies ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (n + 1) - 1 ) )
assume  p in U ; ::_thesis: ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (n + 1) - 1 )
then A20: (f ") . p in (f ") .: U by A18, FUNCT_1:def_6;
 ( f " U = (f ") .: U & f " U is open ) by A8, A10, A12, A15, A16, TOPGRP_1:26, TOPS_2:55;
then consider W being open Subset of T1 such that
A21: (f ") . p in W and
A22: W c= f " U and
A23: Fr W is finite-ind and
A24: ind (Fr W) <= (n + 1) - 1 by A6, A17, A20, Th16;
set FW = Fr W;
A25: ind (T1 | (Fr W)) = ind (Fr W) by A23, Lm5;
 Fr W,f .: (Fr W) are_homeomorphic by A8, METRIZTS:3;
then A26: T1 | (Fr W),T2 | (f .: (Fr W)) are_homeomorphic by METRIZTS:def_1;
then  T2 | (f .: (Fr W)) is finite-ind by A4, A23, A24, A25;
then A27: f .: (Fr W) is finite-ind by Th18;
 F " = f " by A11, A12, TOPS_2:def_4;
then A28: f . ((f ") . p) = p by A10, A12, A16, FUNCT_1:35;
 ind (T2 | (f .: (Fr W))) <= ind (T1 | (Fr W)) by A4, A23, A24, A25, A26;
then A29: ind (T2 | (f .: (Fr W))) <= (n + 1) - 1 by A24, A25, XXREAL_0:2;
reconsider W9 = f .: W as open Subset of T2 by A8, A15, A16, TOPGRP_1:25;
take  W9 ; ::_thesis: ( p in W9 & W9 c= U & Fr W9 is finite-ind & ind (Fr W9) <= (n + 1) - 1 )
 W9 c= f .: (f " U) by A22, RELAT_1:123;
hence  ( p in W9 & W9 c= U ) by A9, A10, A21, A28, FUNCT_1:77, FUNCT_1:def_6; ::_thesis: ( Fr W9 is finite-ind & ind (Fr W9) <= (n + 1) - 1 )
f .: (Fr W) = f .: ((Cl W) \ W) by TOPS_1:42
.= (f .: (Cl W)) \ W9 by A12, FUNCT_1:64
.= (Cl W9) \ W9 by A8, A16, TOPS_2:60
.= Fr W9 by TOPS_1:42 ;
hence  ( Fr W9 is finite-ind & ind (Fr W9) <= (n + 1) - 1 ) by A27, A29, Lm5; ::_thesis: verum
end;
then  T2 is finite-ind by Th15;
hence  ( T2 is finite-ind & ind T2 <= ind T1 ) by A17, A19, Th16; ::_thesis: verum
end;
end;
end;
end;
end;
A30: S1[ 0 ]
proof
let T1, T2 be TopSpace; ::_thesis: ( T1,T2 are_homeomorphic & T1 is finite-ind & ind T1 <= 0 implies ( T2 is finite-ind & ind T2 <= ind T1 ) )
assume that
A31: T1,T2 are_homeomorphic and
A32: T1 is finite-ind and
A33: ind T1 <= 0 ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
consider f being Function of T1,T2 such that
A34: f is being_homeomorphism by A31, T_0TOPSP:def_1;
set f9 = f " ;
A35: dom f = [#] T1 by A34, TOPS_2:def_5;
A36: rng f = [#] T2 by A34, TOPS_2:def_5;
A37: f is onto by A36, FUNCT_2:def_3;
A38: f is one-to-one by A34, TOPS_2:def_5;
percases ( [#] T1 = {} T1 or [#] T1 <> {} T1 ) ;
supposeA39: [#] T1 = {} T1 ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
then  ind T1 = - 1 by Th6;
hence  ( T2 is finite-ind & ind T2 <= ind T1 ) by A36, A39, Def4, Th6; ::_thesis: verum
end;
supposeA40: [#] T1 <> {} T1 ; ::_thesis: ( T2 is finite-ind & ind T2 <= ind T1 )
then  not T1 is empty ;
then reconsider i = ind T1 as Nat by A32;
A41: i = 0 by A33;
A42: not T1 is empty by A40;
A43: not T2 is empty by A35, A40;
then A44: dom (f ") = [#] T2 by A36, A38, TOPS_2:49;
A45: for p being Point of T2
for U being open Subset of T2 st p in U holds
ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 0 - 1 )
proof
reconsider F = f as Function ;
let p be Point of T2; ::_thesis: for U being open Subset of T2 st p in U holds
ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 0 - 1 )
let U be open Subset of T2; ::_thesis: ( p in U implies ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 0 - 1 ) )
assume  p in U ; ::_thesis: ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 0 - 1 )
then A46: (f ") . p in (f ") .: U by A44, FUNCT_1:def_6;
 F " = f " by A37, A38, TOPS_2:def_4;
then A47: f . ((f ") . p) = p by A36, A38, A43, FUNCT_1:35;
 ( f " U = (f ") .: U & f " U is open ) by A34, A36, A38, A42, A43, TOPGRP_1:26, TOPS_2:55;
then consider W being open Subset of T1 such that
A48: (f ") . p in W and
A49: W c= f " U and
A50: Fr W is finite-ind and
A51: ind (Fr W) <= 0 - 1 by A32, A33, A46, Th16;
reconsider W9 = f .: W as open Subset of T2 by A34, A42, A43, TOPGRP_1:25;
take  W9 ; ::_thesis: ( p in W9 & W9 c= U & Fr W9 is finite-ind & ind (Fr W9) <= 0 - 1 )
 W9 c= f .: (f " U) by A49, RELAT_1:123;
hence  ( p in W9 & W9 c= U ) by A35, A36, A47, A48, FUNCT_1:77, FUNCT_1:def_6; ::_thesis: ( Fr W9 is finite-ind & ind (Fr W9) <= 0 - 1 )
 ind (Fr W) >= - 1 by A50, Th5;
then  ind (Fr W) = - 1 by A51, XXREAL_0:1;
then  Fr W = {} T1 by A50, Th6;
then  W is closed by TOPGEN_1:14;
then  W9 is closed by A34, A43, TOPS_2:58;
then  Fr W9 = {} T2 by TOPGEN_1:14;
hence  ( Fr W9 is finite-ind & ind (Fr W9) <= 0 - 1 ) by Th6; ::_thesis: verum
end;
then  T2 is finite-ind by Th15;
hence  ( T2 is finite-ind & ind T2 <= ind T1 ) by A41, A45, Th16; ::_thesis: verum
end;
end;
end;
A52: for n being Nat holds S1[n] from NAT_1:sch_2(A30, A3);
 (ind T1) + 0 <= i by XREAL_1:6;
hence  ( T2 is finite-ind & ind T2 <= ind T1 ) by A1, A2, A52; ::_thesis: verum
end;

Lm9:  for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds
( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) )
proof
let T1, T2 be TopSpace; ::_thesis: ( T1,T2 are_homeomorphic implies ( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) ) )
assume A1: T1,T2 are_homeomorphic ; ::_thesis: ( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) )
consider f being Function of T1,T2 such that
A2: f is being_homeomorphism by A1, T_0TOPSP:def_1;
A3: dom f = [#] T1 by A2, TOPS_2:def_5;
A4: rng f = [#] T2 by A2, TOPS_2:def_5;
percases ( [#] T1 = {} T1 or not T1 is empty ) ;
supposeA5: [#] T1 = {} T1 ; ::_thesis: ( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) )
then  ind ([#] T2) = - 1 by A4, Th6;
hence  ( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) ) by A4, A5, Def4, Th6; ::_thesis: verum
end;
suppose not T1 is empty ; ::_thesis: ( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) )
then reconsider t1 = T1, t2 = T2 as non empty TopSpace by A3;
A6: t2,t1 are_homeomorphic by A1;
hence  ( T1 is finite-ind iff T2 is finite-ind ) by Lm8; ::_thesis: ( T1 is finite-ind implies ind T2 = ind T1 )
assume A7: T1 is finite-ind ; ::_thesis: ind T2 = ind T1
then  T2 is finite-ind by A1, Lm8;
then A8: ind T1 <= ind T2 by A6, Lm8;
 ind T2 <= ind T1 by A1, A7, Lm8;
hence  ind T2 = ind T1 by A8, XXREAL_0:1; ::_thesis: verum
end;
end;
end;

theorem :: TOPDIM_1:23
for n being Nat
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 ) )
proof
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, XBOOLE_1:1;
then  Cl W1 c= A ` by A8, XBOOLE_1:1;
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, XBOOLE_1:1, 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
end;

theorem :: TOPDIM_1:24
for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds
( T1 is finite-ind iff T2 is finite-ind ) by Lm9;

theorem :: TOPDIM_1:25
for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds
ind T1 = ind T2 by Lm9;

theorem Th26: :: TOPDIM_1:26
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is finite-ind iff A2 is finite-ind )
proof
let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is finite-ind iff A2 is finite-ind )
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is finite-ind iff A2 is finite-ind )
let A2 be Subset of T2; ::_thesis: ( A1,A2 are_homeomorphic implies ( A1 is finite-ind iff A2 is finite-ind ) )
assume  A1,A2 are_homeomorphic ; ::_thesis: ( A1 is finite-ind iff A2 is finite-ind )
then A1: T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def_1;
hereby  ::_thesis: ( A2 is finite-ind implies A1 is finite-ind )
assume  A1 is finite-ind ; ::_thesis: A2 is finite-ind
then  T2 | A2 is finite-ind by A1, Lm9;
hence  A2 is finite-ind by Th18; ::_thesis: verum
end;
assume  A2 is finite-ind ; ::_thesis: A1 is finite-ind
then  T1 | A1 is finite-ind by A1, Lm9;
hence  A1 is finite-ind by Th18; ::_thesis: verum
end;

theorem :: TOPDIM_1:27
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic & A1 is finite-ind holds
ind A1 = ind A2
proof
let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic & A1 is finite-ind holds
ind A1 = ind A2
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic & A1 is finite-ind holds
ind A1 = ind A2
let A2 be Subset of T2; ::_thesis: ( A1,A2 are_homeomorphic & A1 is finite-ind implies ind A1 = ind A2 )
assume that
A1: A1,A2 are_homeomorphic and
A2: A1 is finite-ind ; ::_thesis: ind A1 = ind A2
 T1 | A1,T2 | A2 are_homeomorphic by A1, METRIZTS:def_1;
then A3: ind (T1 | A1) = ind (T2 | A2) by A2, Lm9;
 ( A2 is finite-ind & ind (T1 | A1) = ind A1 ) by A1, A2, Lm5, Th26;
hence  ind A1 = ind A2 by A3, Lm5; ::_thesis: verum
end;

theorem :: TOPDIM_1:28
for T1, T2 being TopSpace st [:T1,T2:] is finite-ind holds
( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] )
proof
let T1, T2 be TopSpace; ::_thesis: ( [:T1,T2:] is finite-ind implies ( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] ) )
assume A1: [:T1,T2:] is finite-ind ; ::_thesis: ( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] )
percases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ;
supposeA2: ( T1 is empty or T2 is empty ) ; ::_thesis: ( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] )
then  ind [:T1,T2:] = - 1 by Th6;
hence  ( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] ) by A2, Th6; ::_thesis: verum
end;
suppose ( not T1 is empty & not T2 is empty ) ; ::_thesis: ( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] )
then  [:T1,T2:],[:T2,T1:] are_homeomorphic by YELLOW12:44;
hence  ( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] ) by A1, Lm9; ::_thesis: verum
end;
end;
end;

theorem :: TOPDIM_1:29
for T being TopSpace
for A being Subset of T
for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds
( G is finite-ind & ind G = ind Ga )
proof
let T be TopSpace; ::_thesis: for A being Subset of T
for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds
( G is finite-ind & ind G = ind Ga )
let A be Subset of T; ::_thesis: for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds
( G is finite-ind & ind G = ind Ga )
let G be Subset-Family of T; ::_thesis: for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds
( G is finite-ind & ind G = ind Ga )
let G1 be Subset-Family of (T | A); ::_thesis: ( G1 is finite-ind & G1 = G implies ( G is finite-ind & ind G = ind G1 ) )
assume that
A1: G1 is finite-ind and
A2: G1 = G ; ::_thesis: ( G is finite-ind & ind G = ind G1 )
A3: for B being Subset of T st B in G holds
( B is finite-ind & ind B <= ind G1 )
proof
let B be Subset of T; ::_thesis: ( B in G implies ( B is finite-ind & ind B <= ind G1 ) )
assume A4: B in G ; ::_thesis: ( B is finite-ind & ind B <= ind G1 )
then reconsider B9 = B as Subset of (T | A) by A2;
A5: B9 is finite-ind by A1, A2, A4, Th4;
then  ind B = ind B9 by Th22;
hence  ( B is finite-ind & ind B <= ind G1 ) by A1, A2, A4, A5, Th11, Th22; ::_thesis: verum
end;
A6: - 1 <= ind G1 by A1, Th11;
then A7: ind G <= ind G1 by A3, Th11;
A8: G is finite-ind by A3, A6, Th11;
A9: for B being Subset of (T | A) st B in G1 holds
( B is finite-ind & ind B <= ind G )
proof
let B be Subset of (T | A); ::_thesis: ( B in G1 implies ( B is finite-ind & ind B <= ind G ) )
assume A10: B in G1 ; ::_thesis: ( B is finite-ind & ind B <= ind G )
then reconsider B9 = B as Subset of T by A2;
 B9 is finite-ind by A2, A3, A10;
then  ind B = ind B9 by Th21;
hence  ( B is finite-ind & ind B <= ind G ) by A1, A2, A6, A8, A10, Th11; ::_thesis: verum
end;
 - 1 <= ind G by A8, Th11;
then  ind G1 <= ind G by A9, Th11;
hence  ( G is finite-ind & ind G = ind G1 ) by A3, A6, A7, Th11, XXREAL_0:1; ::_thesis: verum
end;

theorem :: TOPDIM_1:30
for T being TopSpace
for A being Subset of T
for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st G is finite-ind & Ga = G holds
( Ga is finite-ind & ind G = ind Ga )
proof
let T be TopSpace; ::_thesis: for A being Subset of T
for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st G is finite-ind & Ga = G holds
( Ga is finite-ind & ind G = ind Ga )
let A be Subset of T; ::_thesis: for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st G is finite-ind & Ga = G holds
( Ga is finite-ind & ind G = ind Ga )
let G be Subset-Family of T; ::_thesis: for Ga being Subset-Family of (T | A) st G is finite-ind & Ga = G holds
( Ga is finite-ind & ind G = ind Ga )
let G1 be Subset-Family of (T | A); ::_thesis: ( G is finite-ind & G1 = G implies ( G1 is finite-ind & ind G = ind G1 ) )
assume that
A1: G is finite-ind and
A2: G1 = G ; ::_thesis: ( G1 is finite-ind & ind G = ind G1 )
A3: for B being Subset of (T | A) st B in G1 holds
( B is finite-ind & ind B <= ind G )
proof
let B be Subset of (T | A); ::_thesis: ( B in G1 implies ( B is finite-ind & ind B <= ind G ) )
assume A4: B in G1 ; ::_thesis: ( B is finite-ind & ind B <= ind G )
then reconsider B9 = B as Subset of T by A2;
A5: B9 is finite-ind by A1, A2, A4, Th4;
then  ind B = ind B9 by Th21;
hence  ( B is finite-ind & ind B <= ind G ) by A1, A2, A4, A5, Th11, Th21; ::_thesis: verum
end;
A6: - 1 <= ind G by A1, Th11;
then A7: ind G1 <= ind G by A3, Th11;
A8: G1 is finite-ind by A3, A6, Th11;
A9: for B being Subset of T st B in G holds
( B is finite-ind & ind B <= ind G1 )
proof
let B be Subset of T; ::_thesis: ( B in G implies ( B is finite-ind & ind B <= ind G1 ) )
assume A10: B in G ; ::_thesis: ( B is finite-ind & ind B <= ind G1 )
then reconsider B9 = B as Subset of (T | A) by A2;
 B9 is finite-ind by A2, A3, A10;
then  ind B = ind B9 by Th22;
hence  ( B is finite-ind & ind B <= ind G1 ) by A1, A2, A6, A8, A10, Th11; ::_thesis: verum
end;
 - 1 <= ind G1 by A8, Th11;
then  ind G <= ind G1 by A9, Th11;
hence  ( G1 is finite-ind & ind G = ind G1 ) by A3, A6, A7, Th11, XXREAL_0:1; ::_thesis: verum
end;

begin

theorem Th31: :: TOPDIM_1:31
for T being TopSpace
for n being Nat holds
( ( T is finite-ind & ind T <= n ) iff ex Bas being Basis of T st
for A being Subset of T st A in Bas holds
( Fr A is finite-ind & ind (Fr A) <= n - 1 ) )
proof
let T be TopSpace; ::_thesis: for n being Nat holds
( ( T is finite-ind & ind T <= n ) iff ex Bas being Basis of T st
for A being Subset of T st A in Bas holds
( Fr A is finite-ind & ind (Fr A) <= n - 1 ) )
let n be Nat; ::_thesis: ( ( T is finite-ind & ind T <= n ) iff ex Bas being Basis of T st
for A being Subset of T st A in Bas holds
( Fr A is finite-ind & ind (Fr A) <= n - 1 ) )
set TOP = the topology of T;
set cT = the carrier of T;
hereby  ::_thesis: ( ex Bas being Basis of T st
for A being Subset of T st A in Bas holds
( Fr A is finite-ind & ind (Fr A) <= n - 1 ) implies ( T is finite-ind & ind T <= n ) )
defpred S1[ set , set ] means  for p being Point of T
for A being Subset of T st $1 = [p,A] holds
( $2 in the topology of T & ( not p in A implies $2 = {} T ) & ( p in A implies ex W being open Subset of T st
( W = $2 & p in W & W c= A & ind (Fr W) <= n - 1 ) ) );
assume that
A1: T is finite-ind and
A2: ind T <= n ; ::_thesis: ex RNG being Basis of T st
for B being Subset of T st B in RNG holds
( Fr b4 is finite-ind & ind (Fr b4) <= n - 1 )
A3: for x being set st x in [: the carrier of T, the topology of T:] holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in [: the carrier of T, the topology of T:] implies ex y being set st S1[x,y] )
assume  x in [: the carrier of T, the topology of T:] ; ::_thesis: ex y being set st S1[x,y]
then consider p9, A9 being set  such that
A4: p9 in the carrier of T and
A5: A9 in the topology of T and
A6: x = [p9,A9] by ZFMISC_1:def_2;
reconsider p9 = p9 as Point of T by A4;
reconsider A9 = A9 as open Subset of T by A5, PRE_TOPC:def_2;
percases ( not p9 in A9 or p9 in A9 ) ;
supposeA7: not p9 in A9 ; ::_thesis: ex y being set st S1[x,y]
take  {} T ; ::_thesis: S1[x, {} T]
let p be Point of T; ::_thesis: for A being Subset of T st x = [p,A] holds
( {} T in the topology of T & ( not p in A implies {} T = {} T ) & ( p in A implies ex W being open Subset of T st
( W = {} T & p in W & W c= A & ind (Fr W) <= n - 1 ) ) )
let A be Subset of T; ::_thesis: ( x = [p,A] implies ( {} T in the topology of T & ( not p in A implies {} T = {} T ) & ( p in A implies ex W being open Subset of T st
( W = {} T & p in W & W c= A & ind (Fr W) <= n - 1 ) ) ) )
assume A8: x = [p,A] ; ::_thesis: ( {} T in the topology of T & ( not p in A implies {} T = {} T ) & ( p in A implies ex W being open Subset of T st
( W = {} T & p in W & W c= A & ind (Fr W) <= n - 1 ) ) )
 p = p9 by A6, A8, XTUPLE_0:1;
hence  ( {} T in the topology of T & ( not p in A implies {} T = {} T ) & ( p in A implies ex W being open Subset of T st
( W = {} T & p in W & W c= A & ind (Fr W) <= n - 1 ) ) ) by A6, A7, A8, PRE_TOPC:def_2, XTUPLE_0:1; ::_thesis: verum
end;
suppose p9 in A9 ; ::_thesis: ex y being set st S1[x,y]
then consider W being open Subset of T such that
A9: ( p9 in W & W c= A9 ) and
 Fr W is finite-ind and
A10: ind (Fr W) <= n - 1 by A1, A2, Th16;
take  W ; ::_thesis: S1[x,W]
let p be Point of T; ::_thesis: for A being Subset of T st x = [p,A] holds
( W in the topology of T & ( not p in A implies W = {} T ) & ( p in A implies ex W being open Subset of T st
( W = W & p in W & W c= A & ind (Fr W) <= n - 1 ) ) )
let A be Subset of T; ::_thesis: ( x = [p,A] implies ( W in the topology of T & ( not p in A implies W = {} T ) & ( p in A implies ex W being open Subset of T st
( W = W & p in W & W c= A & ind (Fr W) <= n - 1 ) ) ) )
assume  x = [p,A] ; ::_thesis: ( W in the topology of T & ( not p in A implies W = {} T ) & ( p in A implies ex W being open Subset of T st
( W = W & p in W & W c= A & ind (Fr W) <= n - 1 ) ) )
then  ( p = p9 & A = A9 ) by A6, XTUPLE_0:1;
hence  ( W in the topology of T & ( not p in A implies W = {} T ) & ( p in A implies ex W being open Subset of T st
( W = W & p in W & W c= A & ind (Fr W) <= n - 1 ) ) ) by A9, A10, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A11: dom f = [: the carrier of T, the topology of T:] and
A12: for x being set st x in [: the carrier of T, the topology of T:] holds
S1[x,f . x] from CLASSES1:sch_1(A3);
A13: rng f c= the topology of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the topology of T )
assume  y in rng f ; ::_thesis: y in the topology of T
then consider x being set  such that
A14: x in dom f and
A15: f . x = y by FUNCT_1:def_3;
 ex p, A being set st
( p in the carrier of T & A in the topology of T & x = [p,A] ) by A11, A14, ZFMISC_1:def_2;
hence  y in the topology of T by A11, A12, A14, A15; ::_thesis: verum
end;
then reconsider RNG = rng f as Subset-Family of T by XBOOLE_1:1;
now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_
for_p_being_Point_of_T_st_p_in_A_holds_
ex_W_being_Subset_of_T_st_
(_W_in_RNG_&_p_in_W_&_W_c=_A_)
let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds
ex W being Subset of T st
( W in RNG & p in W & W c= A ) )
assume  A is open ; ::_thesis: for p being Point of T st p in A holds
ex W being Subset of T st
( W in RNG & p in W & W c= A )
then A16: A in the topology of T by PRE_TOPC:def_2;
let p be Point of T; ::_thesis: ( p in A implies ex W being Subset of T st
( W in RNG & p in W & W c= A ) )
assume A17: p in A ; ::_thesis: ex W being Subset of T st
( W in RNG & p in W & W c= A )
A18: [p,A] in [: the carrier of T, the topology of T:] by A16, A17, ZFMISC_1:87;
then consider W being open Subset of T such that
A19: ( W = f . [p,A] & p in W & W c= A ) and
 ind (Fr W) <= n - 1 by A12, A17;
reconsider W = W as Subset of T ;
take W = W; ::_thesis: ( W in RNG & p in W & W c= A )
thus  ( W in RNG & p in W & W c= A ) by A11, A18, A19, FUNCT_1:def_3; ::_thesis: verum
end;
then reconsider RNG = RNG as Basis of T by A13, YELLOW_9:32;
take RNG = RNG; ::_thesis: for B being Subset of T st B in RNG holds
( Fr b3 is finite-ind & ind (Fr b3) <= n - 1 )
let B be Subset of T; ::_thesis: ( B in RNG implies ( Fr b2 is finite-ind & ind (Fr b2) <= n - 1 ) )
assume  B in RNG ; ::_thesis: ( Fr b2 is finite-ind & ind (Fr b2) <= n - 1 )
then consider x being set  such that
A20: x in dom f and
A21: f . x = B by FUNCT_1:def_3;
consider p, A being set  such that
A22: p in the carrier of T and
A23: A in the topology of T and
A24: x = [p,A] by A11, A20, ZFMISC_1:def_2;
percases ( p in A or not p in A ) ;
suppose p in A ; ::_thesis: ( Fr b2 is finite-ind & ind (Fr b2) <= n - 1 )
then  ex W being open Subset of T st
( W = f . [p,A] & p in W & W c= A & ind (Fr W) <= n - 1 ) by A11, A12, A20, A23, A24;
hence  ( Fr B is finite-ind & ind (Fr B) <= n - 1 ) by A1, A21, A24; ::_thesis: verum
end;
supposeA25: not p in A ; ::_thesis: ( Fr b2 is finite-ind & ind (Fr b2) <= n - 1 )
A26: not T is empty by A22;
 B = {} T by A11, A12, A20, A21, A22, A23, A24, A25;
then A27: Fr B = {} T by A26, TOPGEN_1:39;
 0 - 1 <= n - 1 by XREAL_1:9;
hence  ( Fr B is finite-ind & ind (Fr B) <= n - 1 ) by A27, Th6; ::_thesis: verum
end;
end;
end;
given B being Basis of T such that A28: for A being Subset of T st A in B holds
( Fr A is finite-ind & ind (Fr A) <= n - 1 ) ; ::_thesis: ( T is finite-ind & ind T <= n )
A29: now__::_thesis:_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_)
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 consider W being Subset of T such that
A30: W in B and
A31: ( p in W & W c= U ) by YELLOW_9:31;
 B c= the topology of T by TOPS_2:64;
then reconsider W = W as open Subset of T by A30, PRE_TOPC:def_2;
take W = 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 & Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A28, A30, A31; ::_thesis: verum
end;
then  T is finite-ind by Th15;
hence  ( T is finite-ind & ind T <= n ) by A29, Th16; ::_thesis: verum
end;

theorem Th32: :: TOPDIM_1:32
for T being TopSpace st T is T_1 & ( for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) ) holds
( T is finite-ind & ind T <= 0 )
proof
let T be TopSpace; ::_thesis: ( T is T_1 & ( for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) ) implies ( T is finite-ind & ind T <= 0 ) )
assume A1: ( T is T_1 & ( for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) ) ) ; ::_thesis: ( T is finite-ind & ind T <= 0 )
A2: now__::_thesis:_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)_<=_0_-_1_)
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) <= 0 - 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) <= 0 - 1 ) )
assume A3: 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) <= 0 - 1 )
reconsider P = {p} as Subset of T by A3, ZFMISC_1:31;
 not p in U ` by A3, XBOOLE_0:def_5;
then A4: P misses U ` by ZFMISC_1:50;
 not T is empty by A3;
then consider A9, B9 being closed Subset of T such that
A5: A9 misses B9 and
A6: A9 \/ B9 = [#] T and
A7: P c= A9 and
A8: U ` c= B9 by A1, A4;
reconsider W = B9 ` as open Subset of T ;
take W = W; ::_thesis: ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 0 - 1 )
 p in P by TARSKI:def_1;
then  ( (U `) ` = U & not p in B9 ) by A5, A7, XBOOLE_0:3;
hence  ( p in W & W c= U ) by A3, A8, SUBSET_1:12, XBOOLE_0:def_5; ::_thesis: ( Fr W is finite-ind & ind (Fr W) <= 0 - 1 )
 B9 = A9 ` by A5, A6, PRE_TOPC:5;
then  Fr B9 = {} T by TOPGEN_1:14;
hence  ( Fr W is finite-ind & ind (Fr W) <= 0 - 1 ) by Th6; ::_thesis: verum
end;
then  T is finite-ind by Th15;
hence  ( T is finite-ind & ind T <= 0 ) by A2, Th16; ::_thesis: verum
end;

theorem Th33: :: TOPDIM_1:33
for X being set
for f being SetSequence of X ex g being SetSequence of X st
( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) ) ) )
proof
let X be set ; ::_thesis: for f being SetSequence of X ex g being SetSequence of X st
( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) ) ) )
let f be SetSequence of X; ::_thesis: ex g being SetSequence of X st
( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) ) ) )
defpred S1[ set , set ] means  for n being Nat st n = $1 holds
ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & $2 = (f . n) \ (union fn) );
A1: for x being set st x in NAT holds
ex y being set st
( y in bool X & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in bool X & S1[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in bool X & S1[x,y] )
then reconsider n = x as Element of NAT ;
deffunc H1( Nat) ->  Element of bool X = f . $1;
set fn =  {  H1(i) where i is Element of NAT : i in n  }  ;
A2:  {  H1(i) where i is Element of NAT : i in n  }  c= bool X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  H1(i) where i is Element of NAT : i in n  }  or z in bool X )
assume  z in  {  H1(i) where i is Element of NAT : i in n  }  ; ::_thesis: z in bool X
then  ex i being Element of NAT st
( z = H1(i) & i in n ) ;
hence  z in bool X ; ::_thesis: verum
end;
A3: n is finite ;
  {  H1(i) where i is Element of NAT : i in n  }  is finite from FRAENKEL:sch_21(A3);
then reconsider fn =  {  H1(i) where i is Element of NAT : i in n  }  as finite Subset-Family of X by A2;
take y = (f . n) \ (union fn); ::_thesis: ( y in bool X & S1[x,y] )
thus  y in bool X ; ::_thesis: S1[x,y]
let m be Nat; ::_thesis: ( m = x implies ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < m  }  & y = (f . m) \ (union fn) ) )
assume A4: m = x ; ::_thesis: ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < m  }  & y = (f . m) \ (union fn) )
set Fn =  {  (f . i) where i is Element of NAT : i < n  }  ;
take  fn ; ::_thesis: ( fn =  {  (f . i) where i is Element of NAT : i < m  }  & y = (f . m) \ (union fn) )
A5: fn c=  {  (f . i) where i is Element of NAT : i < n  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in fn or z in  {  (f . i) where i is Element of NAT : i < n  }  )
assume  z in fn ; ::_thesis: z in  {  (f . i) where i is Element of NAT : i < n  }
then consider i being Element of NAT  such that
A6: z = f . i and
A7: i in n ;
 i < n by A7, NAT_1:44;
hence  z in  {  (f . i) where i is Element of NAT : i < n  }  by A6; ::_thesis: verum
end;
  {  (f . i) where i is Element of NAT : i < n  }  c= fn
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (f . i) where i is Element of NAT : i < n  }  or z in fn )
assume  z in  {  (f . i) where i is Element of NAT : i < n  }  ; ::_thesis: z in fn
then consider i being Element of NAT  such that
A8: z = f . i and
A9: i < n ;
 i in n by A9, NAT_1:44;
hence  z in fn by A8; ::_thesis: verum
end;
hence  ( fn =  {  (f . i) where i is Element of NAT : i < m  }  & y = (f . m) \ (union fn) ) by A4, A5, XBOOLE_0:def_10; ::_thesis: verum
end;
consider g being SetSequence of X such that
A10: for x being set st x in NAT holds
S1[x,g . x] from FUNCT_2:sch_1(A1);
take  g ; ::_thesis: ( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) ) ) )
A11: union (rng f) c= union (rng g)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union (rng f) or y in union (rng g) )
defpred S2[ Nat] means y in f . $1;
assume  y in union (rng f) ; ::_thesis: y in union (rng g)
then consider Y being set  such that
A12: y in Y and
A13: Y in rng f by TARSKI:def_4;
 ex x being set st
( x in dom f & f . x = Y ) by A13, FUNCT_1:def_3;
then A14: ex n being Nat st S2[n] by A12;
consider Min being Nat such that
A15: S2[Min] and
A16: for n being Nat st S2[n] holds
Min <= n from NAT_1:sch_5(A14);
A17: Min in NAT by ORDINAL1:def_12;
then consider fn being finite Subset-Family of X such that
A18: fn =  {  (f . i) where i is Element of NAT : i < Min  }  and
A19: g . Min = (f . Min) \ (union fn) by A10;
 not y in union fn
proof
assume  y in union fn ; ::_thesis: contradiction
then consider Z being set  such that
A20: y in Z and
A21: Z in fn by TARSKI:def_4;
 ex i being Element of NAT st
( Z = f . i & i < Min ) by A18, A21;
hence  contradiction by A16, A20; ::_thesis: verum
end;
then A22: y in g . Min by A15, A19, XBOOLE_0:def_5;
 dom g = NAT by FUNCT_2:def_1;
then  g . Min in rng g by A17, FUNCT_1:def_3;
hence  y in union (rng g) by A22, TARSKI:def_4; ::_thesis: verum
end;
 union (rng g) c= union (rng f)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union (rng g) or y in union (rng f) )
assume  y in union (rng g) ; ::_thesis: y in union (rng f)
then consider Y being set  such that
A23: y in Y and
A24: Y in rng g by TARSKI:def_4;
consider x being set  such that
A25: x in dom g and
A26: g . x = Y by A24, FUNCT_1:def_3;
reconsider n = x as Nat by A25;
 ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) ) by A10, A25;
then A27: y in f . n by A23, A26, XBOOLE_0:def_5;
 dom f = NAT by FUNCT_2:def_1;
then  f . n in rng f by A25, FUNCT_1:def_3;
hence  y in union (rng f) by A27, TARSKI:def_4; ::_thesis: verum
end;
hence  union (rng f) = union (rng g) by A11, XBOOLE_0:def_10; ::_thesis: ( ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) ) ) )
A28: for i, j being Nat st i < j holds
g . i misses g . j
proof
let i, j be Nat; ::_thesis: ( i < j implies g . i misses g . j )
assume A29: i < j ; ::_thesis: g . i misses g . j
 j in NAT by ORDINAL1:def_12;
then consider fj being finite Subset-Family of X such that
A30: fj =  {  (f . n) where n is Element of NAT : n < j  }  and
A31: g . j = (f . j) \ (union fj) by A10;
assume  g . i meets g . j ; ::_thesis: contradiction
then consider x being set  such that
A32: x in g . i and
A33: x in g . j by XBOOLE_0:3;
A34: i in NAT by ORDINAL1:def_12;
then  ex fi being finite Subset-Family of X st
( fi =  {  (f . n) where n is Element of NAT : n < i  }  & g . i = (f . i) \ (union fi) ) by A10;
then A35: x in f . i by A32, XBOOLE_0:def_5;
 f . i in fj by A29, A30, A34;
then  x in union fj by A35, TARSKI:def_4;
hence  contradiction by A31, A33, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  for i, j being Nat st i <> j holds
g . i misses g . j ::_thesis: for n being Nat ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) )
proof
let i, j be Nat; ::_thesis: ( i <> j implies g . i misses g . j )
assume  i <> j ; ::_thesis: g . i misses g . j
then  ( i < j or j < i ) by XXREAL_0:1;
hence  g . i misses g . j by A28; ::_thesis: verum
end;
let n be Nat; ::_thesis: ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) )
 n in NAT by ORDINAL1:def_12;
hence  ex fn being finite Subset-Family of X st
( fn =  {  (f . i) where i is Element of NAT : i < n  }  & g . n = (f . n) \ (union fn) ) by A10; ::_thesis: verum
end;

theorem Th34: :: TOPDIM_1:34
for T being TopSpace st T is finite-ind & ind T <= 0 & T is Lindelof holds
for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
proof
let T be TopSpace; ::_thesis: ( T is finite-ind & ind T <= 0 & T is Lindelof implies for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) )
assume that
A1: ( T is finite-ind & ind T <= 0 ) and
A2: T is Lindelof ; ::_thesis: for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
set CT = [#] T;
let A, B be closed Subset of T; ::_thesis: ( A misses B implies ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) )
assume A3: A misses B ; ::_thesis: ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
percases ( [#] T = {} or [#] T <> {} ) ;
supposeA4: [#] T = {} ; ::_thesis: ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
take  A ; ::_thesis: ex B9 being closed Subset of T st
( A misses B9 & A \/ B9 = [#] T & A c= A & B c= B9 )
take  B ; ::_thesis: ( A misses B & A \/ B = [#] T & A c= A & B c= B )
thus  ( A misses B & A \/ B = [#] T & A c= A & B c= B ) by A3, A4; ::_thesis: verum
end;
supposeA5: [#] T <> {} ; ::_thesis: ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
defpred S1[ set , set ] means ( $1 is Point of T & $1 in $2 & $2 is open closed Subset of T & ( $2 c= A ` or $2 c= B ` ) );
A6: for x being set st x in [#] T holds
ex y being set st
( y in bool ([#] T) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [#] T implies ex y being set st
( y in bool ([#] T) & S1[x,y] ) )
assume A7: x in [#] T ; ::_thesis: ex y being set st
( y in bool ([#] T) & S1[x,y] )
reconsider p = x as Point of T by A7;
percases ( p in A ` or not p in A ` ) ;
suppose p in A ` ; ::_thesis: ex y being set st
( y in bool ([#] T) & S1[x,y] )
then consider W being open Subset of T such that
A8: ( p in W & W c= A ` ) and
A9: Fr W is finite-ind and
A10: ind (Fr W) <= 0 - 1 by A1, Th16;
take  W ; ::_thesis: ( W in bool ([#] T) & S1[x,W] )
thus  W in bool ([#] T) ; ::_thesis: S1[x,W]
 - 1 <= ind (Fr W) by A9, Th5;
then  ind (Fr W) = - 1 by A10, XXREAL_0:1;
then  Fr W = {} T by A9, Th6;
hence  S1[x,W] by A8, TOPGEN_1:14; ::_thesis: verum
end;
supposeA11: not p in A ` ; ::_thesis: ex y being set st
( y in bool ([#] T) & S1[x,y] )
A12: A c= B ` by A3, SUBSET_1:23;
 p in A by A7, A11, XBOOLE_0:def_5;
then consider W being open Subset of T such that
A13: ( p in W & W c= B ` ) and
A14: Fr W is finite-ind and
A15: ind (Fr W) <= 0 - 1 by A1, A12, Th16;
take  W ; ::_thesis: ( W in bool ([#] T) & S1[x,W] )
thus  W in bool ([#] T) ; ::_thesis: S1[x,W]
 - 1 <= ind (Fr W) by A14, Th5;
then  ind (Fr W) = - 1 by A15, XXREAL_0:1;
then  Fr W = {} T by A14, Th6;
hence  S1[x,W] by A13, TOPGEN_1:14; ::_thesis: verum
end;
end;
end;
consider F being Function of ([#] T),(bool ([#] T)) such that
A16: for x being set st x in [#] T holds
S1[x,F . x] from FUNCT_2:sch_1(A6);
reconsider RNG = rng F as Subset-Family of T ;
A17: dom F = [#] T by FUNCT_2:def_1;
 [#] T c= union RNG
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] T or x in union RNG )
assume A18: x in [#] T ; ::_thesis: x in union RNG
reconsider p = x as Point of T by A18;
 ( p in F . p & F . p in RNG ) by A16, A17, A18, FUNCT_1:def_3;
hence  x in union RNG by TARSKI:def_4; ::_thesis: verum
end;
then  [#] T = union RNG by XBOOLE_0:def_10;
then A19: RNG is Cover of T by SETFAM_1:45;
 RNG is open
proof
let U be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not U in RNG or U is open )
assume  U in RNG ; ::_thesis: U is open
then  ex x being set st
( x in dom F & F . x = U ) by FUNCT_1:def_3;
hence  U is open by A16; ::_thesis: verum
end;
then consider G being Subset-Family of T such that
A20: G c= RNG and
A21: G is Cover of T and
A22: G is countable by A2, A19, METRIZTS:def_2;
 not T is empty by A5;
then A23: not G is empty by A21, TOPS_2:3;
then consider U being Function of NAT,G such that
A24: rng U = G by A22, CARD_3:96;
A25: dom U = NAT by A23, FUNCT_2:def_1;
then reconsider U = U as SetSequence of ([#] T) by A24, FUNCT_2:2;
consider V being SetSequence of ([#] T) such that
A26: union (rng U) = union (rng V) and
A27: for i, j being Nat st i <> j holds
V . i misses V . j and
A28: for n being Nat ex Un being finite Subset-Family of ([#] T) st
( Un =  {  (U . i) where i is Element of NAT : i < n  }  & V . n = (U . n) \ (union Un) ) by Th33;
reconsider rngV = rng V as Subset-Family of T ;
set AA =  {  (V . n) where n is Element of NAT : V . n misses B  }  ;
A29:  {  (V . n) where n is Element of NAT : V . n misses B  }  c= rng V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (V . n) where n is Element of NAT : V . n misses B  }  or x in rng V )
assume  x in  {  (V . n) where n is Element of NAT : V . n misses B  }  ; ::_thesis: x in rng V
then  ( dom V = NAT & ex n being Element of NAT st
( x = V . n & V . n misses B ) ) by FUNCT_2:def_1;
hence  x in rng V by FUNCT_1:def_3; ::_thesis: verum
end;
then reconsider AA =  {  (V . n) where n is Element of NAT : V . n misses B  }  as Subset-Family of T by XBOOLE_1:1;
set BB = rngV \ AA;
A30: rngV is open
proof
let A be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not A in rngV or A is open )
assume  A in rngV ; ::_thesis: A is open
then consider m being set  such that
A31: m in dom V and
A32: V . m = A by FUNCT_1:def_3;
reconsider m = m as Element of NAT by A31;
consider Un being finite Subset-Family of ([#] T) such that
A33: Un =  {  (U . i) where i is Element of NAT : i < m  }  and
A34: V . m = (U . m) \ (union Un) by A28;
reconsider Un = Un as Subset-Family of T ;
 U . m in rng U by A25, FUNCT_1:def_3;
then  ex x being set st
( x in dom F & F . x = U . m ) by A20, A24, FUNCT_1:def_3;
then reconsider UN = U . m as open Subset of T by A16;
 Un is closed
proof
let D be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not D in Un or D is closed )
assume  D in Un ; ::_thesis: D is closed
then  ex i being Element of NAT st
( D = U . i & i < m ) by A33;
then  D in rng U by A25, FUNCT_1:def_3;
then  ex x being set st
( x in dom F & F . x = D ) by A20, A24, FUNCT_1:def_3;
hence  D is closed by A16; ::_thesis: verum
end;
then  union Un is closed by TOPS_2:21;
then  UN /\ ((union Un) `) is open ;
hence  A is open by A32, A34, SUBSET_1:13; ::_thesis: verum
end;
then  union AA is open by A29, TOPS_2:11, TOPS_2:19;
then reconsider UAA = union AA, UBB = union (rngV \ AA) as open Subset of T by A30, TOPS_2:15, TOPS_2:19;
A35: UAA misses UBB
proof
assume  UAA meets UBB ; ::_thesis: contradiction
then consider x being set  such that
A36: x in union AA and
A37: x in union (rngV \ AA) by XBOOLE_0:3;
consider Ax being set  such that
A38: x in Ax and
A39: Ax in AA by A36, TARSKI:def_4;
consider n being Element of NAT  such that
A40: V . n = Ax and
A41: V . n misses B by A39;
consider Bx being set  such that
A42: x in Bx and
A43: Bx in rngV \ AA by A37, TARSKI:def_4;
 Bx in rngV by A43, XBOOLE_0:def_5;
then consider m being set  such that
A44: m in dom V and
A45: V . m = Bx by FUNCT_1:def_3;
reconsider m = m as Element of NAT by A44;
 not Bx in AA by A43, XBOOLE_0:def_5;
then  m <> n by A41, A45;
then  V . n misses V . m by A27;
hence  contradiction by A38, A40, A42, A45, XBOOLE_0:3; ::_thesis: verum
end;
 rngV = (rngV \ AA) \/ AA by A29, XBOOLE_1:45;
then A46: UAA \/ UBB = union G by A24, A26, ZFMISC_1:78
.= [#] T by A21, SETFAM_1:45 ;
then A47: UAA = UBB ` by A35, PRE_TOPC:5;
 B misses UAA
proof
assume  B meets UAA ; ::_thesis: contradiction
then consider x being set  such that
A48: x in B and
A49: x in union AA by XBOOLE_0:3;
consider Ax being set  such that
A50: x in Ax and
A51: Ax in AA by A49, TARSKI:def_4;
 ex n being Element of NAT st
( V . n = Ax & V . n misses B ) by A51;
hence  contradiction by A48, A50, XBOOLE_0:3; ::_thesis: verum
end;
then A52: B c= UAA ` by SUBSET_1:23;
 A misses UBB
proof
assume  A meets UBB ; ::_thesis: contradiction
then consider x being set  such that
A53: x in A and
A54: x in union (rngV \ AA) by XBOOLE_0:3;
consider Bx being set  such that
A55: x in Bx and
A56: Bx in rngV \ AA by A54, TARSKI:def_4;
 Bx in rngV by A56, XBOOLE_0:def_5;
then consider m being set  such that
A57: m in dom V and
A58: V . m = Bx by FUNCT_1:def_3;
reconsider m = m as Element of NAT by A57;
 not V . m in AA by A56, A58, XBOOLE_0:def_5;
then  V . m meets B ;
then consider b being set  such that
A59: b in V . m and
A60: b in B by XBOOLE_0:3;
 U . m in rng U by A25, FUNCT_1:def_3;
then consider p being set  such that
A61: p in dom F and
A62: F . p = U . m by A20, A24, FUNCT_1:def_3;
reconsider Fp = F . p as Subset of T by A62;
A63: ex Un being finite Subset of (bool ([#] T)) st
( Un =  {  (U . i) where i is Element of NAT : i < m  }  & V . m = (U . m) \ (union Un) ) by A28;
then  b in U . m by A59, XBOOLE_0:def_5;
then  Fp meets B by A60, A62, XBOOLE_0:3;
then  not Fp c= B ` by SUBSET_1:23;
then A64: U . m c= A ` by A16, A61, A62;
 x in U . m by A55, A58, A63, XBOOLE_0:def_5;
hence  contradiction by A53, A64, XBOOLE_0:def_5; ::_thesis: verum
end;
then  A c= UAA by A47, SUBSET_1:23;
hence  ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) by A35, A46, A47, A52; ::_thesis: verum
end;
end;
end;

theorem Th35: :: TOPDIM_1:35
for T being TopSpace st T is T_1 & T is Lindelof holds
( ( T is finite-ind & ind T <= 0 ) iff for A, B being closed Subset of T st A misses B holds
{} T separates A,B )
proof
let T be TopSpace; ::_thesis: ( T is T_1 & T is Lindelof implies ( ( T is finite-ind & ind T <= 0 ) iff for A, B being closed Subset of T st A misses B holds
{} T separates A,B ) )
assume that
A1: T is T_1 and
A2: T is Lindelof ; ::_thesis: ( ( T is finite-ind & ind T <= 0 ) iff for A, B being closed Subset of T st A misses B holds
{} T separates A,B )
hereby  ::_thesis: ( ( for A, B being closed Subset of T st A misses B holds
{} T separates A,B ) implies ( T is finite-ind & ind T <= 0 ) )
assume A3: ( T is finite-ind & ind T <= 0 ) ; ::_thesis: for A, B being closed Subset of T st A misses B holds
{} T separates A,B
let A, B be closed Subset of T; ::_thesis: ( A misses B implies {} T separates A,B )
assume  A misses B ; ::_thesis: {} T separates A,B
then consider A9, B9 being closed Subset of T such that
A4: A9 misses B9 and
A5: A9 \/ B9 = [#] T and
A6: ( A c= A9 & B c= B9 ) by A2, A3, Th34;
A7: A9 ` = B9 by A4, A5, PRE_TOPC:5;
 ( (A9 \/ B9) ` = (({} T) `) ` & A9 = B9 ` ) by A4, A5, PRE_TOPC:5;
hence  {} T separates A,B by A4, A6, A7, METRIZTS:def_3; ::_thesis: verum
end;
assume A8: for A, B being closed Subset of T st A misses B holds
{} T separates A,B ; ::_thesis: ( T is finite-ind & ind T <= 0 )
 for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
proof
let A, B be closed Subset of T; ::_thesis: ( A misses B implies ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) )
assume  A misses B ; ::_thesis: ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
then  {} T separates A,B by A8;
then consider U, W being open Subset of T such that
A9: ( A c= U & B c= W ) and
A10: U misses W and
A11: {} T = (U \/ W) ` by METRIZTS:def_3;
A12: [#] T = ((U \/ W) `) ` by A11
.= U \/ W ;
then  ( U = W ` & W = U ` ) by A10, PRE_TOPC:5;
hence  ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) by A9, A10, A12; ::_thesis: verum
end;
hence  ( T is finite-ind & ind T <= 0 ) by A1, Th32; ::_thesis: verum
end;

theorem :: TOPDIM_1:36
for T being TopSpace st T is T_4 & T is Lindelof & ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= 0 ) holds
( T is finite-ind & ind T <= 0 )
proof
let T be TopSpace; ::_thesis: ( T is T_4 & T is Lindelof & ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= 0 ) implies ( T is finite-ind & ind T <= 0 ) )
assume that
A1: T is T_4 and
A2: T is Lindelof ; ::_thesis: ( for F being Subset-Family of T holds
( not F is closed or not F is Cover of T or not F is countable or not F is finite-ind or not ind F <= 0 ) or ( T is finite-ind & ind T <= 0 ) )
set CT = [#] T;
given F being Subset-Family of T such that A3: F is closed and
A4: F is Cover of T and
A5: F is countable and
A6: ( F is finite-ind & ind F <= 0 ) ; ::_thesis: ( T is finite-ind & ind T <= 0 )
percases ( union F is empty or not union F is empty ) ;
suppose union F is empty ; ::_thesis: ( T is finite-ind & ind T <= 0 )
then  [#] T = {} T by A4, SETFAM_1:45;
hence  ( T is finite-ind & ind T <= 0 ) by Def4, Th6; ::_thesis: verum
end;
supposeA7: not union F is empty ; ::_thesis: ( T is finite-ind & ind T <= 0 )
then reconsider CT = [#] T as non empty set ;
consider f being Function of NAT,F such that
A8: F = rng f by A5, A7, CARD_3:96, ZFMISC_1:2;
A9: dom f = NAT by A7, FUNCT_2:def_1, ZFMISC_1:2;
now__::_thesis:_for_A,_B_being_closed_Subset_of_T_st_A_misses_B_holds_
ex_unionG,_unionH_being_closed_Subset_of_T_st_
(_unionG_misses_unionH_&_unionG_\/_unionH_=_[#]_T_&_A_c=_unionG_&_B_c=_unionH_)
set CTT = [:(bool CT),(bool CT):];
defpred S1[ set , set ] means  for n being Nat
for A, B being Subset of T st $1 = [n,[A,B]] holds
( ( Cl A meets Cl B implies $2 = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & $2 = [G,H] & Cl G misses Cl H ) ) );
set TOP = the topology of T;
let A, B be closed Subset of T; ::_thesis: ( A misses B implies ex unionG, unionH being closed Subset of T st
( unionG misses unionH & unionG \/ unionH = [#] T & A c= unionG & B c= unionH ) )
assume A10: A misses B ; ::_thesis: ex unionG, unionH being closed Subset of T st
( unionG misses unionH & unionG \/ unionH = [#] T & A c= unionG & B c= unionH )
A11: ( Cl A = A & Cl B = B ) by PRE_TOPC:22;
A12: for x being set st x in [:NAT,[:(bool CT),(bool CT):]:] holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in [:NAT,[:(bool CT),(bool CT):]:] implies ex y being set st S1[x,y] )
assume  x in [:NAT,[:(bool CT),(bool CT):]:] ; ::_thesis: ex y being set st S1[x,y]
then consider n9, ab being set  such that
A13: n9 in NAT and
A14: ab in [:(bool CT),(bool CT):] and
A15: x = [n9,ab] by ZFMISC_1:def_2;
consider A9, B9 being set  such that
A16: ( A9 in bool CT & B9 in bool CT ) and
A17: ab = [A9,B9] by A14, ZFMISC_1:def_2;
reconsider A9 = A9, B9 = B9 as Subset of T by A16;
percases ( Cl A9 meets Cl B9 or Cl A9 misses Cl B9 ) ;
supposeA18: Cl A9 meets Cl B9 ; ::_thesis: ex y being set st S1[x,y]
take  ab ; ::_thesis: S1[x,ab]
let n be Nat; ::_thesis: for A, B being Subset of T st x = [n,[A,B]] holds
( ( Cl A meets Cl B implies ab = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & ab = [G,H] & Cl G misses Cl H ) ) )
let A, B be Subset of T; ::_thesis: ( x = [n,[A,B]] implies ( ( Cl A meets Cl B implies ab = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & ab = [G,H] & Cl G misses Cl H ) ) ) )
assume  x = [n,[A,B]] ; ::_thesis: ( ( Cl A meets Cl B implies ab = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & ab = [G,H] & Cl G misses Cl H ) ) )
then A19: ab = [A,B] by A15, XTUPLE_0:1;
then  A = A9 by A17, XTUPLE_0:1;
hence  ( ( Cl A meets Cl B implies ab = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & ab = [G,H] & Cl G misses Cl H ) ) ) by A17, A18, A19, XTUPLE_0:1; ::_thesis: verum
end;
supposeA20: Cl A9 misses Cl B9 ; ::_thesis: ex y being set st S1[x,y]
A21: f . n9 in rng f by A9, A13, FUNCT_1:def_3;
then reconsider fn = f . n9 as Subset of T by A8;
A22: fn is closed by A3, A21, TOPS_2:def_2;
A23: fn is finite-ind by A6, A21, Th11;
then A24: ind (T | fn) = ind fn by Lm5;
A25: ind fn <= 0 by A6, A21, Th11;
A26: [#] (T | fn) = fn by PRE_TOPC:def_5;
then reconsider Af = (Cl A9) /\ fn, Bf = (Cl B9) /\ fn as Subset of (T | fn) by XBOOLE_1:17;
A27: ( Af is closed & Bf is closed ) by A26, PRE_TOPC:13;
 Af misses Bf by A20, XBOOLE_1:76;
then consider AF, BF being closed Subset of (T | fn) such that
A28: AF misses BF and
A29: AF \/ BF = [#] (T | fn) and
A30: Af c= AF and
A31: Bf c= BF by A2, A22, A25, A23, A24, A27, Th34;
 [#] (T | fn) c= [#] T by PRE_TOPC:def_4;
then reconsider af = AF, bf = BF as Subset of T by XBOOLE_1:1;
A32: af \/ (Cl A9) misses bf \/ (Cl B9)
proof
assume  af \/ (Cl A9) meets bf \/ (Cl B9) ; ::_thesis: contradiction
then consider x being set  such that
A33: ( x in af \/ (Cl A9) & x in bf \/ (Cl B9) ) by XBOOLE_0:3;
percases ( ( x in af & x in bf ) or ( x in Cl A9 & x in Cl B9 ) or ( x in af & x in Cl B9 ) or ( x in bf & x in Cl A9 ) ) by A33, XBOOLE_0:def_3;
suppose ( ( x in af & x in bf ) or ( x in Cl A9 & x in Cl B9 ) ) ; ::_thesis: contradiction
hence  contradiction by A20, A28, XBOOLE_0:3; ::_thesis: verum
end;
supposeA34: ( x in af & x in Cl B9 ) ; ::_thesis: contradiction
then  x in Bf by A26, XBOOLE_0:def_4;
hence  contradiction by A28, A31, A34, XBOOLE_0:3; ::_thesis: verum
end;
supposeA35: ( x in bf & x in Cl A9 ) ; ::_thesis: contradiction
then  x in Af by A26, XBOOLE_0:def_4;
hence  contradiction by A28, A30, A35, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
 ( bf is closed & af is closed ) by A22, A26, TSEP_1:8;
then consider U, W being open Subset of T such that
A36: af \/ (Cl A9) c= U and
A37: bf \/ (Cl B9) c= W and
A38: Cl U misses Cl W by A1, A32, Th2;
take uw = [U,W]; ::_thesis: S1[x,uw]
let n be Nat; ::_thesis: for A, B being Subset of T st x = [n,[A,B]] holds
( ( Cl A meets Cl B implies uw = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & uw = [G,H] & Cl G misses Cl H ) ) )
let A, B be Subset of T; ::_thesis: ( x = [n,[A,B]] implies ( ( Cl A meets Cl B implies uw = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & uw = [G,H] & Cl G misses Cl H ) ) ) )
assume A39: x = [n,[A,B]] ; ::_thesis: ( ( Cl A meets Cl B implies uw = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & uw = [G,H] & Cl G misses Cl H ) ) )
then A40: n = n9 by A15, XTUPLE_0:1;
A41: ab = [A,B] by A15, A39, XTUPLE_0:1;
then  B = B9 by A17, XTUPLE_0:1;
then A42: Cl B c= W by A37, XBOOLE_1:11;
 ( af c= U & bf c= W ) by A36, A37, XBOOLE_1:11;
then A43: f . n c= U \/ W by A26, A29, A40, XBOOLE_1:13;
A44: A = A9 by A17, A41, XTUPLE_0:1;
then  Cl A c= U by A36, XBOOLE_1:11;
hence  ( ( Cl A meets Cl B implies uw = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & uw = [G,H] & Cl G misses Cl H ) ) ) by A17, A20, A38, A41, A42, A43, A44, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
consider GH being Function such that
 dom GH = [:NAT,[:(bool CT),(bool CT):]:] and
A45: for x being set st x in [:NAT,[:(bool CT),(bool CT):]:] holds
S1[x,GH . x] from CLASSES1:sch_1(A12);
deffunc H1( set , set ) ->  set = GH . [$1,$2];
consider ghSeq being Function such that
A46: dom ghSeq = NAT and
A47: ghSeq . 0 = [A,B] and
A48: for n being Nat holds ghSeq . (n + 1) = H1(n,ghSeq . n) from NAT_1:sch_11();
defpred S2[ Nat] means ( ghSeq . $1 in [:(bool CT),(bool CT):] & ( for A, B being Subset of T st A = (ghSeq . $1) `1 & B = (ghSeq . $1) `2 holds
Cl A misses Cl B ) );
A49: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A50: S2[n] ; ::_thesis: S2[n + 1]
consider A, B being set  such that
A51: ( A in bool CT & B in bool CT ) and
A52: ghSeq . n = [A,B] by A50, ZFMISC_1:def_2;
reconsider A = A, B = B as Subset of T by A51;
 n in NAT by ORDINAL1:def_12;
then A53: [n,(ghSeq . n)] in [:NAT,[:(bool CT),(bool CT):]:] by A50, ZFMISC_1:87;
 ( A = [A,B] `1 & B = [A,B] `2 ) ;
then  Cl A misses Cl B by A50, A52;
then consider G, H being open Subset of T such that
 f . n c= G \/ H and
 Cl A c= G and
 Cl B c= H and
A54: GH . [n,(ghSeq . n)] = [G,H] and
A55: Cl G misses Cl H by A45, A52, A53;
A56: ghSeq . (n + 1) = [G,H] by A48, A54;
 ( G = [G,H] `1 & [G,H] `2 = H ) ;
hence  S2[n + 1] by A55, A56; ::_thesis: verum
end;
 ( A = [A,B] `1 & B = [A,B] `2 ) ;
then A57: S2[ 0 ] by A10, A11, A47;
A58: for n being Nat holds S2[n] from NAT_1:sch_2(A57, A49);
 rng ghSeq c= [:(bool CT),(bool CT):]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ghSeq or y in [:(bool CT),(bool CT):] )
assume  y in rng ghSeq ; ::_thesis: y in [:(bool CT),(bool CT):]
then  ex x being set st
( x in dom ghSeq & ghSeq . x = y ) by FUNCT_1:def_3;
hence  y in [:(bool CT),(bool CT):] by A46, A58; ::_thesis: verum
end;
then reconsider ghSeq = ghSeq as Function of NAT,[:(bool CT),(bool CT):] by A46, FUNCT_2:2;
set g = pr1 ghSeq;
set h = pr2 ghSeq;
A59: (pr2 ghSeq) . 0 = [A,B] `2 by A47, FUNCT_2:def_6
.= B ;
reconsider RngH = rng ((pr2 ghSeq) ^\ 1), RngG = rng ((pr1 ghSeq) ^\ 1) as Subset-Family of T ;
A60: (pr1 ghSeq) . 0 = [A,B] `1 by A47, FUNCT_2:def_5
.= A ;
A61: for n being Nat holds
( (pr1 ghSeq) . (n + 1) in the topology of T & (pr2 ghSeq) . (n + 1) in the topology of T & (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) & (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) & (pr1 ghSeq) . n misses (pr2 ghSeq) . n & f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) )
proof
let n be Nat; ::_thesis: ( (pr1 ghSeq) . (n + 1) in the topology of T & (pr2 ghSeq) . (n + 1) in the topology of T & (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) & (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) & (pr1 ghSeq) . n misses (pr2 ghSeq) . n & f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) )
consider A, B being set  such that
A62: ( A in bool CT & B in bool CT ) and
A63: ghSeq . n = [A,B] by ZFMISC_1:def_2;
reconsider A = A, B = B as Subset of T by A62;
A64: n in NAT by ORDINAL1:def_12;
then A65: [n,(ghSeq . n)] in [:NAT,[:(bool CT),(bool CT):]:] by ZFMISC_1:87;
A66: A = [A,B] `1 ;
then A67: A = (pr1 ghSeq) . n by A46, A64, A63, MCART_1:def_12;
A68: B = [A,B] `2 ;
then A69: B = (pr2 ghSeq) . n by A46, A64, A63, MCART_1:def_13;
 Cl A misses Cl B by A58, A66, A68, A63;
then consider G, H being open Subset of T such that
A70: f . n c= G \/ H and
A71: Cl A c= G and
A72: Cl B c= H and
A73: GH . [n,(ghSeq . n)] = [G,H] and
 Cl G misses Cl H by A45, A63, A65;
A74: ghSeq . (n + 1) = [G,H] by A48, A73;
A75: G = [G,H] `1
.= (pr1 ghSeq) . (n + 1) by A46, A74, MCART_1:def_12 ;
hence  (pr1 ghSeq) . (n + 1) in the topology of T by PRE_TOPC:def_2; ::_thesis: ( (pr2 ghSeq) . (n + 1) in the topology of T & (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) & (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) & (pr1 ghSeq) . n misses (pr2 ghSeq) . n & f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) )
A76: H = [G,H] `2
.= (pr2 ghSeq) . (n + 1) by A46, A74, MCART_1:def_13 ;
hence  (pr2 ghSeq) . (n + 1) in the topology of T by PRE_TOPC:def_2; ::_thesis: ( (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) & (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) & (pr1 ghSeq) . n misses (pr2 ghSeq) . n & f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) )
 A c= Cl A by PRE_TOPC:18;
hence  (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) by A67, A71, A75, XBOOLE_1:1; ::_thesis: ( (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) & (pr1 ghSeq) . n misses (pr2 ghSeq) . n & f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) )
 B c= Cl B by PRE_TOPC:18;
hence  (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) by A69, A72, A76, XBOOLE_1:1; ::_thesis: ( (pr1 ghSeq) . n misses (pr2 ghSeq) . n & f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) )
 ( A c= Cl A & B c= Cl B ) by PRE_TOPC:18;
hence  (pr1 ghSeq) . n misses (pr2 ghSeq) . n by A58, A66, A67, A68, A69, A63, XBOOLE_1:64; ::_thesis: f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1))
thus  f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) by A70, A75, A76; ::_thesis: verum
end;
then  for n being Element of NAT holds (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) ;
then A77: pr1 ghSeq is non-descending by KURATO_0:def_4;
A78: RngH is open
proof
A79: RngH =  {  ((pr2 ghSeq) . n) where n is Element of NAT : n >= 1  }  by SETLIM_1:6;
let A be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not A in RngH or A is open )
assume  A in RngH ; ::_thesis: A is open
then consider n being Element of NAT  such that
A80: (pr2 ghSeq) . n = A and
A81: n >= 1 by A79;
reconsider n1 = n - 1 as Nat by A81, NAT_1:21;
 (pr2 ghSeq) . (n1 + 1) in the topology of T by A61;
hence  A is open by A80, PRE_TOPC:def_2; ::_thesis: verum
end;
 RngG is open
proof
A82: RngG =  {  ((pr1 ghSeq) . n) where n is Element of NAT : n >= 1  }  by SETLIM_1:6;
let A be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not A in RngG or A is open )
assume  A in RngG ; ::_thesis: A is open
then consider n being Element of NAT  such that
A83: (pr1 ghSeq) . n = A and
A84: n >= 1 by A82;
reconsider n1 = n - 1 as Nat by A84, NAT_1:21;
 (pr1 ghSeq) . (n1 + 1) in the topology of T by A61;
hence  A is open by A83, PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider unionG = union RngG, unionH = union RngH as open Subset of T by A78, TOPS_2:19;
 for n being Element of NAT holds (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) by A61;
then A85: pr2 ghSeq is non-descending by KURATO_0:def_4;
A86: unionH misses unionG
proof
assume  unionH meets unionG ; ::_thesis: contradiction
then consider x being set  such that
A87: x in unionH and
A88: x in unionG by XBOOLE_0:3;
consider H being set  such that
A89: x in H and
A90: H in RngH by A87, TARSKI:def_4;
 RngH =  {  ((pr2 ghSeq) . n) where n is Element of NAT : n >= 1  }  by SETLIM_1:6;
then consider i being Element of NAT  such that
A91: (pr2 ghSeq) . i = H and
 i >= 1 by A90;
consider G being set  such that
A92: x in G and
A93: G in RngG by A88, TARSKI:def_4;
 RngG =  {  ((pr1 ghSeq) . n) where n is Element of NAT : n >= 1  }  by SETLIM_1:6;
then consider j being Element of NAT  such that
A94: (pr1 ghSeq) . j = G and
 j >= 1 by A93;
percases ( i <= j or i >= j ) ;
supposeA95: i <= j ; ::_thesis: contradiction
A96: (pr1 ghSeq) . j misses (pr2 ghSeq) . j by A61;
 (pr2 ghSeq) . i c= (pr2 ghSeq) . j by A85, A95, PROB_1:def_5;
hence  contradiction by A92, A94, A89, A91, A96, XBOOLE_0:3; ::_thesis: verum
end;
supposeA97: i >= j ; ::_thesis: contradiction
A98: (pr1 ghSeq) . i misses (pr2 ghSeq) . i by A61;
 (pr1 ghSeq) . j c= (pr1 ghSeq) . i by A77, A97, PROB_1:def_5;
hence  contradiction by A92, A94, A89, A91, A98, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
A99: CT c= unionH \/ unionG
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in CT or x in unionH \/ unionG )
assume  x in CT ; ::_thesis: x in unionH \/ unionG
then reconsider x = x as Point of T ;
 union F = CT by A4, SETFAM_1:45;
then consider X being set  such that
A100: x in X and
A101: X in rng f by A8, TARSKI:def_4;
consider n being set  such that
A102: n in dom f and
A103: f . n = X by A101, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A102;
A104: n + 1 >= 1 by NAT_1:12;
A105: f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) by A61;
percases ( x in (pr1 ghSeq) . (n + 1) or x in (pr2 ghSeq) . (n + 1) ) by A100, A103, A105, XBOOLE_0:def_3;
supposeA106: x in (pr1 ghSeq) . (n + 1) ; ::_thesis: x in unionH \/ unionG
 RngG =  {  ((pr1 ghSeq) . i) where i is Element of NAT : i >= 1  }  by SETLIM_1:6;
then  (pr1 ghSeq) . (n + 1) in RngG by A104;
then  x in unionG by A106, TARSKI:def_4;
hence  x in unionH \/ unionG by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA107: x in (pr2 ghSeq) . (n + 1) ; ::_thesis: x in unionH \/ unionG
 RngH =  {  ((pr2 ghSeq) . i) where i is Element of NAT : i >= 1  }  by SETLIM_1:6;
then  (pr2 ghSeq) . (n + 1) in RngH by A104;
then  x in unionH by A107, TARSKI:def_4;
hence  x in unionH \/ unionG by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then  CT = unionH \/ unionG by XBOOLE_0:def_10;
then  ( unionH = unionG ` & unionG = unionH ` ) by A86, PRE_TOPC:5;
then reconsider unionG = unionG, unionH = unionH as closed Subset of T ;
take unionG = unionG; ::_thesis: ex unionH being closed Subset of T st
( unionG misses unionH & unionG \/ unionH = [#] T & A c= unionG & B c= unionH )
take unionH = unionH; ::_thesis: ( unionG misses unionH & unionG \/ unionH = [#] T & A c= unionG & B c= unionH )
thus  unionG misses unionH by A86; ::_thesis: ( unionG \/ unionH = [#] T & A c= unionG & B c= unionH )
thus  unionG \/ unionH = [#] T by A99, XBOOLE_0:def_10; ::_thesis: ( A c= unionG & B c= unionH )
 RngG =  {  ((pr1 ghSeq) . i) where i is Element of NAT : i >= 1  }  by SETLIM_1:6;
then  (pr1 ghSeq) . 1 in RngG ;
then A108: (pr1 ghSeq) . 1 c= unionG by ZFMISC_1:74;
 (pr1 ghSeq) . 0 c= (pr1 ghSeq) . (0 + 1) by A61;
hence  A c= unionG by A108, A60, XBOOLE_1:1; ::_thesis: B c= unionH
 RngH =  {  ((pr2 ghSeq) . i) where i is Element of NAT : i >= 1  }  by SETLIM_1:6;
then  (pr2 ghSeq) . 1 in RngH ;
then A109: (pr2 ghSeq) . 1 c= unionH by ZFMISC_1:74;
 (pr2 ghSeq) . 0 c= (pr2 ghSeq) . (0 + 1) by A61;
hence  B c= unionH by A109, A59, XBOOLE_1:1; ::_thesis: verum
end;
hence  ( T is finite-ind & ind T <= 0 ) by A1, Th32; ::_thesis: verum
end;
end;
end;

theorem Th37: :: TOPDIM_1:37
for TM being metrizable TopSpace
for A, B being closed Subset of TM st A misses B holds
for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds
ex L being Subset of TM st
( L separates A,B & L misses Null )
proof
let TM be metrizable TopSpace; ::_thesis: for A, B being closed Subset of TM st A misses B holds
for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds
ex L being Subset of TM st
( L separates A,B & L misses Null )
let A, B be closed Subset of TM; ::_thesis: ( A misses B implies for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds
ex L being Subset of TM st
( L separates A,B & L misses Null ) )
assume  A misses B ; ::_thesis: for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds
ex L being Subset of TM st
( L separates A,B & L misses Null )
then consider U, W being open Subset of TM such that
A1: ( A c= U & B c= W ) and
A2: Cl U misses Cl W by Th2;
let Null be finite-ind Subset of TM; ::_thesis: ( ind Null <= 0 & TM | Null is second-countable implies ex L being Subset of TM st
( L separates A,B & L misses Null ) )
assume A3: ( ind Null <= 0 & TM | Null is second-countable ) ; ::_thesis: ex L being Subset of TM st
( L separates A,B & L misses Null )
set TN = TM | Null;
A4: [#] (TM | Null) = Null by PRE_TOPC:def_5;
then reconsider Un = (Cl U) /\ Null, Wn = (Cl W) /\ Null as Subset of (TM | Null) by XBOOLE_1:17;
 ( Un c= Cl U & Wn c= Cl W ) by XBOOLE_1:17;
then A5: Un misses Wn by A2, XBOOLE_1:64;
A6: ind (TM | Null) = ind Null by Lm5;
 ( Un is closed & Wn is closed ) by A4, TSP_1:def_2;
then  {} (TM | Null) separates Un,Wn by A3, A5, A6, Th35;
then consider L being Subset of TM such that
A7: L separates A,B and
A8: Null /\ L c= {} (TM | Null) by A1, A2, METRIZTS:26;
take  L ; ::_thesis: ( L separates A,B & L misses Null )
 Null /\ L = {} by A8;
hence  ( L separates A,B & L misses Null ) by A7, XBOOLE_0:def_7; ::_thesis: verum
end;

theorem Th38: :: TOPDIM_1:38
for TM being metrizable TopSpace
for Null being Subset of TM st TM | Null is second-countable holds
( ( Null is finite-ind & ind Null <= 0 ) 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 & Null misses Fr W ) )
proof
let TM be metrizable TopSpace; ::_thesis: for Null being Subset of TM st TM | Null is second-countable holds
( ( Null is finite-ind & ind Null <= 0 ) 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 & Null misses Fr W ) )
let Null be Subset of TM; ::_thesis: ( TM | Null is second-countable implies ( ( Null is finite-ind & ind Null <= 0 ) 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 & Null misses Fr W ) ) )
assume A1: TM | Null is second-countable ; ::_thesis: ( ( Null is finite-ind & ind Null <= 0 ) 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 & Null misses Fr W ) )
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 & Null misses Fr W ) ) implies ( Null is finite-ind & ind Null <= 0 ) )
assume A2: ( Null is finite-ind & ind Null <= 0 ) ; ::_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 & Null misses Fr W )
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 & Null misses Fr W )
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 & Null misses Fr W ) )
assume A3: p in U ; ::_thesis: ex W being open Subset of TM st
( p in W & W c= U & Null misses Fr W )
reconsider P = {p} as Subset of TM by A3, ZFMISC_1:31;
 not p in U ` by A3, XBOOLE_0:def_5;
then A4: P misses U ` by ZFMISC_1:50;
 not TM is empty by A3;
then consider L being Subset of TM such that
A5: L separates P,U ` and
A6: L misses Null by A1, A2, A4, Th37;
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 & Null misses Fr W )
 ( W c= W1 ` & W1 ` c= (U `) ` ) by A8, A9, SUBSET_1:12, SUBSET_1:23;
hence  ( p in W & W c= U ) by A7, XBOOLE_1:1, ZFMISC_1:31; ::_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:23;
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:42;
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:36; ::_thesis: verum
end;
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: ( Null is finite-ind & ind Null <= 0 )
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 )
proof
let p be Point of (TM | Null); ::_thesis: 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 U be open Subset of (TM | Null); ::_thesis: ( p in U implies 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 ) )
assume A17: p in U ; ::_thesis: 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 )
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: ( p in W & W c= U & Fr W is finite-ind & 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 finite-ind & ind (Fr W) <= 0 - 1 )
A23: (Fr W9) /\ Null = {} by A22, XBOOLE_0:def_7;
 Fr W c= (Fr W9) /\ Null by A18, Th1;
hence  ( Fr W is finite-ind & ind (Fr W) <= 0 - 1 ) by A23, Th6; ::_thesis: verum
end;
then A24: TM | Null is finite-ind by Th15;
then A25: Null is finite-ind by Th18;
 ind (TM | Null) <= 0 by A16, A24, Th16;
hence  ( Null is finite-ind & ind Null <= 0 ) by A25, Lm5; ::_thesis: verum
end;

theorem Th39: :: TOPDIM_1:39
for TM being metrizable TopSpace
for Null being Subset of TM st TM | Null is second-countable holds
( ( Null is finite-ind & ind Null <= 0 ) iff ex B being Basis of TM st
for A being Subset of TM st A in B holds
Null misses Fr A )
proof
let TM be metrizable TopSpace; ::_thesis: for Null being Subset of TM st TM | Null is second-countable holds
( ( Null is finite-ind & ind Null <= 0 ) iff ex B being Basis of TM st
for A being Subset of TM st A in B holds
Null misses Fr A )
set cTM = [#] TM;
set TOP = the topology of TM;
let Null be Subset of TM; ::_thesis: ( TM | Null is second-countable implies ( ( Null is finite-ind & ind Null <= 0 ) iff ex B being Basis of TM st
for A being Subset of TM st A in B holds
Null misses Fr A ) )
assume A1: TM | Null is second-countable ; ::_thesis: ( ( Null is finite-ind & ind Null <= 0 ) iff ex B being Basis of TM st
for A being Subset of TM st A in B holds
Null misses Fr A )
hereby  ::_thesis: ( ex B being Basis of TM st
for A being Subset of TM st A in B holds
Null misses Fr A implies ( Null is finite-ind & ind Null <= 0 ) )
defpred S1[ set , set ] means  for p being Point of TM
for A being Subset of TM st $1 = [p,A] holds
( $2 in the topology of TM & ( not p in A implies $2 = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = $2 & p in W & W c= A & Null misses Fr W ) ) );
assume A2: ( Null is finite-ind & ind Null <= 0 ) ; ::_thesis: ex RNG being Basis of TM st
for B being Subset of TM st B in RNG holds
Null misses Fr b4
A3: for x being set st x in [:([#] TM), the topology of TM:] holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in [:([#] TM), the topology of TM:] implies ex y being set st S1[x,y] )
assume  x in [:([#] TM), the topology of TM:] ; ::_thesis: ex y being set st S1[x,y]
then consider p9, A9 being set  such that
A4: p9 in [#] TM and
A5: A9 in the topology of TM and
A6: x = [p9,A9] by ZFMISC_1:def_2;
reconsider p9 = p9 as Point of TM by A4;
reconsider A9 = A9 as open Subset of TM by A5, PRE_TOPC:def_2;
percases ( not p9 in A9 or p9 in A9 ) ;
supposeA7: not p9 in A9 ; ::_thesis: ex y being set st S1[x,y]
take  {} TM ; ::_thesis: S1[x, {} TM]
let p be Point of TM; ::_thesis: for A being Subset of TM st x = [p,A] holds
( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & Null misses Fr W ) ) )
let A be Subset of TM; ::_thesis: ( x = [p,A] implies ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & Null misses Fr W ) ) ) )
assume A8: x = [p,A] ; ::_thesis: ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & Null misses Fr W ) ) )
 p = p9 by A6, A8, XTUPLE_0:1;
hence  ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & Null misses Fr W ) ) ) by A6, A7, A8, PRE_TOPC:def_2, XTUPLE_0:1; ::_thesis: verum
end;
suppose p9 in A9 ; ::_thesis: ex y being set st S1[x,y]
then consider W being open Subset of TM such that
A9: ( p9 in W & W c= A9 & Null misses Fr W ) by A1, A2, Th38;
take  W ; ::_thesis: S1[x,W]
let p be Point of TM; ::_thesis: for A being Subset of TM st x = [p,A] holds
( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & Null misses Fr W ) ) )
let A be Subset of TM; ::_thesis: ( x = [p,A] implies ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & Null misses Fr W ) ) ) )
assume  x = [p,A] ; ::_thesis: ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & Null misses Fr W ) ) )
then  ( p = p9 & A = A9 ) by A6, XTUPLE_0:1;
hence  ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & Null misses Fr W ) ) ) by A9, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A10: dom f = [:([#] TM), the topology of TM:] and
A11: for x being set st x in [:([#] TM), the topology of TM:] holds
S1[x,f . x] from CLASSES1:sch_1(A3);
A12: rng f c= the topology of TM
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the topology of TM )
assume  y in rng f ; ::_thesis: y in the topology of TM
then consider x being set  such that
A13: x in dom f and
A14: f . x = y by FUNCT_1:def_3;
 ex p, A being set st
( p in [#] TM & A in the topology of TM & x = [p,A] ) by A10, A13, ZFMISC_1:def_2;
hence  y in the topology of TM by A10, A11, A13, A14; ::_thesis: verum
end;
then reconsider RNG = rng f as Subset-Family of TM by XBOOLE_1:1;
now__::_thesis:_for_A_being_Subset_of_TM_st_A_is_open_holds_
for_p_being_Point_of_TM_st_p_in_A_holds_
ex_W_being_Subset_of_TM_st_
(_W_in_RNG_&_p_in_W_&_W_c=_A_)
let A be Subset of TM; ::_thesis: ( A is open implies for p being Point of TM st p in A holds
ex W being Subset of TM st
( W in RNG & p in W & W c= A ) )
assume  A is open ; ::_thesis: for p being Point of TM st p in A holds
ex W being Subset of TM st
( W in RNG & p in W & W c= A )
then A15: A in the topology of TM by PRE_TOPC:def_2;
let p be Point of TM; ::_thesis: ( p in A implies ex W being Subset of TM st
( W in RNG & p in W & W c= A ) )
assume A16: p in A ; ::_thesis: ex W being Subset of TM st
( W in RNG & p in W & W c= A )
A17: [p,A] in [:([#] TM), the topology of TM:] by A15, A16, ZFMISC_1:87;
then consider W being open Subset of TM such that
A18: ( W = f . [p,A] & p in W & W c= A ) and
 Null misses Fr W by A11, A16;
reconsider W = W as Subset of TM ;
take W = W; ::_thesis: ( W in RNG & p in W & W c= A )
thus  ( W in RNG & p in W & W c= A ) by A10, A17, A18, FUNCT_1:def_3; ::_thesis: verum
end;
then reconsider RNG = RNG as Basis of TM by A12, YELLOW_9:32;
take RNG = RNG; ::_thesis: for B being Subset of TM st B in RNG holds
Null misses Fr b3
let B be Subset of TM; ::_thesis: ( B in RNG implies Null misses Fr b2 )
assume  B in RNG ; ::_thesis: Null misses Fr b2
then consider x being set  such that
A19: x in dom f and
A20: f . x = B by FUNCT_1:def_3;
consider p, A being set  such that
A21: p in [#] TM and
A22: A in the topology of TM and
A23: x = [p,A] by A10, A19, ZFMISC_1:def_2;
percases ( p in A or not p in A ) ;
suppose p in A ; ::_thesis: Null misses Fr b2
then  ex W being open Subset of TM st
( W = f . [p,A] & p in W & W c= A & Null misses Fr W ) by A10, A11, A19, A22, A23;
hence  Null misses Fr B by A20, A23; ::_thesis: verum
end;
suppose not p in A ; ::_thesis: Null misses Fr b2
then  B = {} TM by A10, A11, A19, A20, A21, A22, A23;
then  Fr B = {} TM by TOPGEN_1:14;
hence  Null misses Fr B by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
given B being Basis of TM such that A24: for A being Subset of TM st A in B holds
Null misses Fr A ; ::_thesis: ( Null is finite-ind & ind Null <= 0 )
 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 )
proof
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 & Null misses Fr W )
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 & Null misses Fr W ) )
assume  p in U ; ::_thesis: ex W being open Subset of TM st
( p in W & W c= U & Null misses Fr W )
then consider a being Subset of TM such that
A25: a in B and
A26: ( p in a & a c= U ) by YELLOW_9:31;
 B c= the topology of TM by TOPS_2:64;
then reconsider a = a as open Subset of TM by A25, PRE_TOPC:def_2;
take  a ; ::_thesis: ( p in a & a c= U & Null misses Fr a )
thus  ( p in a & a c= U & Null misses Fr a ) by A24, A25, A26; ::_thesis: verum
end;
hence  ( Null is finite-ind & ind Null <= 0 ) by A1, Th38; ::_thesis: verum
end;

theorem :: TOPDIM_1:40
for TM being metrizable TopSpace
for Null, A being Subset of TM st TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 holds
( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )
proof
let TM be metrizable TopSpace; ::_thesis: for Null, A being Subset of TM st TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 holds
( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )
let Null, A be Subset of TM; ::_thesis: ( TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 implies ( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 ) )
assume that
A1: TM | Null is second-countable and
A2: Null is finite-ind and
A3: A is finite-ind and
A4: ind Null <= 0 ; ::_thesis: ( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )
set TAN = TM | (A \/ Null);
A5: [#] (TM | (A \/ Null)) = A \/ Null by PRE_TOPC:def_5;
then reconsider N9 = Null, A9 = A as Subset of (TM | (A \/ Null)) by XBOOLE_1:7;
A6: ind N9 = ind Null by A2, Th21;
 ( N9 is finite-ind & (TM | (A \/ Null)) | N9 is second-countable ) by A1, A2, Th21, METRIZTS:9;
then consider B being Basis of (TM | (A \/ Null)) such that
A7: for b being Subset of (TM | (A \/ Null)) st b in B holds
N9 misses Fr b by A4, A6, Th39;
set i = ind A;
 - 1 <= ind A by A3, Th5;
then  (- 1) + 1 <= (ind A) + 1 by XREAL_1:6;
then reconsider i1 = (ind A) + 1 as Element of NAT by INT_1:3;
A8: ( A9 is finite-ind & ind A9 = ind A ) by A3, Th21;
A9: for b being Subset of (TM | (A \/ Null)) st b in B holds
( Fr b is finite-ind & ind (Fr b) <= i1 - 1 )
proof
let b be Subset of (TM | (A \/ Null)); ::_thesis: ( b in B implies ( Fr b is finite-ind & ind (Fr b) <= i1 - 1 ) )
assume  b in B ; ::_thesis: ( Fr b is finite-ind & ind (Fr b) <= i1 - 1 )
then  N9 misses Fr b by A7;
then  Fr b c= A9 by A5, XBOOLE_1:73;
hence  ( Fr b is finite-ind & ind (Fr b) <= i1 - 1 ) by A8, Th19; ::_thesis: verum
end;
then  TM | (A \/ Null) is finite-ind by Th31;
then A10: A \/ Null is finite-ind by Th18;
 ind (TM | (A \/ Null)) <= i1 by A9, Th31;
hence  ( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 ) by A10, Lm5; ::_thesis: verum
end;