:: Small {I}nductive {D}imension of {T}opological {S}paces
::  by Karol P\c{a}k
::
:: Received June 29, 2009
:: Copyright (c) 2009-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, PRE_TOPC, SUBSET_1, RELAT_1, SETFAM_1, RCOMP_1, NAT_1,
      INT_1, XBOOLE_0, TOPS_1, TARSKI, PROB_1, ZFMISC_1, STRUCT_0, FUNCT_1,
      CARD_1, ARYTM_3, PARTFUN1, FINSET_1, XXREAL_0, COMPTS_1, ARYTM_1,
      ORDINAL1, T_0TOPSP, TOPS_2, CARD_5, METRIZTS, RLVECT_3, CARD_3, MCART_1,
      PCOMPS_1, WAYBEL23, TOPDIM_1, FUNCT_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, ORDINAL1,
      XTUPLE_0, MCART_1, FUNCT_2, CARD_1, CARD_3, CANTOR_1, FINSET_1, NUMBERS,
      ZFMISC_1, XXREAL_0, XCMPLX_0, REAL_1, SETFAM_1, DOMAIN_1, PRE_TOPC,
      TOPS_1, TOPS_2, INT_1, NAT_1, STRUCT_0, COMPTS_1, PCOMPS_1, PROB_1,
      WAYBEL23, BORSUK_1, BORSUK_3, METRIZTS;
 constructors TOPS_1, TOPS_2, BORSUK_1, REAL_1, CANTOR_1, WAYBEL23, COMPTS_1,
      BORSUK_3, METRIZTS, PCOMPS_1, KURATO_0, EUCLID, XTUPLE_0;
 registrations BORSUK_3, CARD_1, COMPTS_1, FINSET_1, FUNCT_2, INT_1, NAT_1,
      ORDINAL1, PRE_TOPC, STRUCT_0, SUBSET_1, TOPREAL6, TOPS_1, XCMPLX_0,
      XREAL_0, XXREAL_0, YELLOW13, METRIZTS, RELSET_1, BORSUK_1, XTUPLE_0;
 requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
 definitions TOPS_2, TARSKI, XBOOLE_0;
 equalities COMPTS_1, STRUCT_0, SUBSET_1, TOPS_1, XBOOLE_0, CARD_1, ORDINAL1;
 expansions TOPS_2, TARSKI, XBOOLE_0, FUNCT_2;
 theorems CARD_2, CARD_3, FUNCT_1, FUNCT_2, INT_1, ORDINAL1, MCART_1, NAT_1,
      PRE_TOPC, PROB_1, RELAT_1, SETFAM_1, SETLIM_1, SUBSET_1, TARSKI,
      TOPGEN_1, TOPGRP_1, TOPS_1, TOPS_2, TOPS_3, TSEP_1, TSP_1, T_0TOPSP,
      XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, YELLOW12, YELLOW_9, ZFMISC_1,
      METRIZTS, KURATO_0, XTUPLE_0;
 schemes CLASSES1, FRAENKEL, FUNCT_2, NAT_1, SUBSET_1;

begin :: Preliminaries

reserve T,T1,T2 for TopSpace,
  A,B for Subset of T,
  F for Subset of T|A,
  G,G1, G2 for Subset-Family of T,
  U,W for open Subset of T|A,
  p for Point of T|A,
  n for Nat,
  I for Integer;

theorem Th1:
  F = B/\A implies Fr F c= Fr B/\A
proof
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;
  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 thesis by XBOOLE_1:16;
end;

theorem Th2:
  T is normal iff for A,B be closed Subset of T st A misses B ex U,
  W be open Subset of T st A c=U & B c=W & Cl U misses Cl W
proof
  hereby
    assume
A1: T is normal;
    let A1,A2 be closed Subset of T;
    assume A1 misses A2;
    then consider B1,B2 be 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 be 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 be 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,D1 as open Subset of T by A13,A7;
    take C1,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;
    Cl D2`=D2` & D2`c=B2 by A14,A16,PRE_TOPC:22,SUBSET_1:17;
    then Cl D1 c=B2 by A18;
    hence A1 c=C1 & A2 c=D1 & Cl C1 misses Cl D1 by A6,A15,A9,A19,XBOOLE_1:64;
  end;
  assume
A20: for A,B be closed Subset of T st A misses B ex U,W be open Subset
  of T st A c=U & B c=W & Cl U misses Cl W;
  for A,B be Subset of T st A is closed & B is closed & A misses B ex U,W
  be 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;
    assume A is closed & B is closed & A misses B;
    then consider U,W be open Subset of T such that
A21: A c=U & B c=W & Cl U misses Cl W by A20;
    take U,W;
    U c=Cl U & W c=Cl W by PRE_TOPC:18;
    hence thesis by A21,XBOOLE_1:64;
  end;
  hence thesis by PRE_TOPC:def 12;
end;

::  The sequence of a subset family of topological spaces
::  with limited small inductive dimension

definition
  let T;
  func Seq_of_ind T -> SetSequence of ((bool the carrier of T) qua set)
       means
  :Def1:
  it.0
= { {}T } & ( A in it.(n+1) iff A in it.n or for p,U st p in U ex W st p in W &
  W c=U & Fr W in it.n);
  existence
  proof
    defpred P[object,object] means
    ex D1,D2 being set st D1= $1 & D2 = $2 &
    for A holds A in D2 iff A in D1 or for p,U st p in U ex W st
    p in W & W c=U & Fr W in D1;
    set C = the carrier of T;
    reconsider E={{}T} as Element of bool bool C;
A1: for x be object st x in bool bool C
   ex y be object st y in bool bool C & P[x ,y]
    proof
      let x be object such that
      x in bool bool C;
       reconsider xx = x as set by TARSKI:1;
      defpred Q[object] means
      for A st A=$1 holds A in xx or for p,U st p in U ex
      W st p in W & W c=U & Fr W in xx;
      consider y be Subset of bool C such that
A2:   for z be set holds z in y iff z in bool C & Q[z] from SUBSET_1:
      sch 1;
      take y;
      thus y in bool bool C;
       reconsider yy = y as set;
      take xx,yy;
      thus xx = x & yy = y;
      let A;
      A in y iff Q[A] by A2;
      hence thesis;
    end;
    consider p be Function of bool bool C,bool bool C such that
A3: for x be object st x in bool bool C holds P[x,p.x] from FUNCT_2:sch 1
    (A1);
    deffunc F(set,set)=p/.$2;
    consider f be sequence of bool bool C such that
A4: f.0=E and
A5: for n holds f.(n+1)=F(n,f.n) from NAT_1:sch 12;
     reconsider f as SetSequence of ((bool the carrier of T) qua set);
    take f;
    now
      let n;
A6:    f.(n+1)=p/.(f.n) by A5
        .=p.(f.n);
       P[f.n,p.(f.n)] by A3;
      hence A in f.(n+1) iff A in f.n or for p,U st p in U ex W st p in W & W
      c=U & Fr W in f.n by A6;
    end;
    hence thesis by A4;
  end;
  uniqueness
  proof
    let Ind1,Ind2 be SetSequence of bool (the carrier of T) qua set
       such that
A7: Ind1.0={{}T} & (A in Ind1.(n+1) iff A in Ind1.n or for p,U st p in
    U ex W st p in W & W c=U & Fr W in Ind1.n) and
A8: Ind2.0={{}T} & (A in Ind2.(n+1) iff A in Ind2.n or for p,U st p
    in U ex W st p in W & W c=U & Fr W in Ind2.n);
    defpred P[Nat] means Ind1.$1=Ind2.$1;
A9: for n be Nat st P[n] holds P[n+1]
    proof
      let n be Nat such that
A10:   P[n];
      thus Ind1.(n+1)c=Ind2.(n+1)
      proof
        let x be object such that
A11:    x in Ind1.(n+1);
        reconsider A=x as Subset of T by A11;
        A in Ind1.n or for p be Point of T|A,U be open Subset of T|A st p
in U ex W be open Subset of T|A st p in W & W c=U & Fr W in Ind1.n by A7,A11;
        hence thesis by A8,A10;
      end;
      let x be object such that
A12:  x in Ind2.(n+1);
      reconsider A=x as Subset of T by A12;
      A in Ind2.n or for p be Point of T|A,U be open Subset of T|A st p
in U ex W be open Subset of T|A st p in W & W c=U & Fr W in Ind2.n by A8,A12;
      hence thesis by A7,A10;
    end;
A13: P[0] by A7,A8;
    for n be Nat holds P[n] from NAT_1:sch 2(A13,A9);
    hence thesis;
  end;
end;

registration
  let T;
  cluster Seq_of_ind T -> non-descending;
  coherence
  proof
    for n be Nat holds (Seq_of_ind T).n c=(Seq_of_ind T).(n+1) by Def1;
    hence thesis by KURATO_0:def 4;
  end;
end;

theorem Th3:
  for F st F = B holds F in (Seq_of_ind T|A).n iff B in (Seq_of_ind T).n
proof
  defpred P[Nat] means for F be Subset of T|A,B st F=B holds F in (Seq_of_ind
  T|A).$1 iff B in (Seq_of_ind T).$1;
A1: for n st P[n] holds P[n+1]
  proof
    set TA=T|A;
    let n such that
A2: P[n];
    set n1=n+1;
    let F be Subset of TA,B such that
A3: F=B;
    set TAF=(T|A)|F;
    set TB=T|B;
A4: TAF=TB by A3,METRIZTS:9;
A5: [#]TB c=[#]T by PRE_TOPC:def 4;
    hereby
      assume
A6:   F in (Seq_of_ind TA).n1;
      per cases by A6,Def1;
      suppose
        F in (Seq_of_ind TA).n;
        then B in (Seq_of_ind T).n by A2,A3;
        hence B in (Seq_of_ind T).n1 by Def1;
      end;
      suppose
A7:     for p be Point of TAF,U be open Subset of TAF st p in U ex W
        be open Subset of TAF st p in W & W c=U & Fr W in (Seq_of_ind TA).n;
        now
          let p be Point of TB,U be open Subset of TB such that
A8:       p in U;
          reconsider U9=U as open Subset of TAF by A4;
          consider W9 be open Subset of TAF such that
A9:       p in W9 & W9 c=U9 & Fr W9 in (Seq_of_ind TA).n by A7,A8;
          reconsider W=W9 as open Subset of TB by A4;
          take W;
          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;
        end;
        hence B in (Seq_of_ind T).n1 by Def1;
      end;
    end;
A10: [#]TAF c=[#]TA by PRE_TOPC:def 4;
    assume
A11: B in (Seq_of_ind T).n1;
    per cases by A11,Def1;
    suppose
      B in (Seq_of_ind T).n;
      then F in (Seq_of_ind TA).n by A2,A3;
      hence F in (Seq_of_ind TA).n1 by Def1;
    end;
    suppose
A12:  for p be Point of TB,U be open Subset of TB st p in U ex W be
      open Subset of TB st p in W & W c=U & Fr W in (Seq_of_ind T).n;
      now
        let p be Point of TAF,U be open Subset of TAF such that
A13:    p in U;
        reconsider U9=U as open Subset of TB by A4;
        consider W9 be open Subset of TB 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 TAF by A4;
        take W;
        Fr W is Subset of TA by A10,XBOOLE_1:1;
        hence p in W & W c=U & Fr W in (Seq_of_ind TA).n by A2,A4,A14;
      end;
      hence F in (Seq_of_ind TA).n1 by Def1;
    end;
  end;
A15: P[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,B;
    assume F=B;
    hence thesis by A16;
  end;
  for n holds P[n] from NAT_1:sch 2(A15,A1);
  hence thesis;
end;

definition
  let T,A;
  attr A is with_finite_small_inductive_dimension means
  :Def2:
  ex n st A in ( Seq_of_ind T).n;
end;

notation
  let T,A;
  synonym A is finite-ind for A is with_finite_small_inductive_dimension;
end;

definition
  let T,G;
  attr G is with_finite_small_inductive_dimension means

  ex n st G c=( Seq_of_ind T).n;
end;

notation
  let T,G;
  synonym G is finite-ind for G is with_finite_small_inductive_dimension;
end;

theorem
  A in G & G is finite-ind implies A is finite-ind;

Lm1: for T be TopSpace,A be finite Subset of T holds A is finite-ind & A in (
Seq_of_ind T).card A
proof
  defpred P[Nat] means for T be TopSpace,A be 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,A be finite Subset of T;
A1: for n st P[n] holds P[n+1]
  proof
    let n such that
A2: P[n];
    let T be TopSpace,A be finite Subset of T such that
A3: card A<=n+1;
    per cases by A3,NAT_1:8;
    suppose
      card A<=n;
      hence thesis by A2;
    end;
    suppose
A4:   card A=n+1;
      for p be Point of T|A,U be open Subset of T|A st p in U ex W be 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,U be open Subset of T|A such that
A5:     p in U;
        take W=U;
        {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;
        [#](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 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;
        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;
        (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 thesis;
      end;
      then A in (Seq_of_ind T).(card A) by A4,Def1;
      hence thesis;
    end;
  end;
A12: P[0]
  proof
    let T be TopSpace,A be finite Subset of T;
A13: (Seq_of_ind T).0={{}T} by Def1;
    assume
A14: card A<=0;
    then A={};
    then A in {{}T} by TARSKI:def 1;
    hence thesis by A13,A14;
  end;
  for n holds P[n] from NAT_1:sch 2(A12,A1);
  then P[card A];
  hence thesis;
end;

registration
  let T;
  cluster finite -> finite-ind for Subset of T;
  coherence by Lm1;
  cluster empty -> finite-ind for Subset-Family of T;
  coherence
  proof
    let G;
    assume G is empty;
    then
A1: G c={{}T};
    (Seq_of_ind T).0={{}T} by Def1;
    hence thesis by A1;
  end;
  cluster non empty finite-ind for Subset-Family of T;
  existence
  proof
    (Seq_of_ind T).0={{}T} by Def1;
    then {{}T} is finite-ind;
    hence thesis;
  end;
end;

registration
  let T be non empty TopSpace;
  cluster non empty finite-ind for Subset of T;
  existence
  proof
    consider x be object such that
A1: x in [#]T by XBOOLE_0:def 1;
    {x} is Subset of T by A1,ZFMISC_1:31;
    hence thesis;
  end;
end;

definition
  let T;
  attr T is with_finite_small_inductive_dimension means
  :Def4:
  [#]T is with_finite_small_inductive_dimension;
end;

notation
  let T;
  synonym T is finite-ind for T is with_finite_small_inductive_dimension;
end;

registration
  cluster empty -> finite-ind for TopSpace;
  coherence;
end;

Lm2: for X be set holds X in (Seq_of_ind 1TopSp X).1
proof
  let X be set;
  set T=1TopSp X;
  set CT=[#]T;
  now
    let p be Point of T|CT,U be open Subset of T|CT such that
A1: p in U;
    take W=U;
A2: [#](T|CT)=CT by PRE_TOPC:def 5;
    then reconsider W9=U as Subset of T;
    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={}T by TOPGEN_1:14;
    then
A3: Fr W9/\CT={};
    W=W/\[#]T by A2,XBOOLE_1:28;
    then Fr W c={}T by A3,Th1;
    then
A4: Fr W={}T;
    (Seq_of_ind T).0={{}T} by Def1;
    hence p in W & W c=U & Fr W in (Seq_of_ind T).0 by A1,A4,TARSKI:def 1;
  end;
  then CT in (Seq_of_ind T).(0+1) by Def1;
  hence thesis;
end;

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

registration
  cluster non empty finite-ind for TopSpace;
  existence
  proof
    take 1TopSp the non empty set;
    thus thesis;
  end;
end;

reserve Af for finite-ind Subset of T,
  Tf for finite-ind TopSpace;

begin :: Concept of the Small Inductive Dimension

definition
  let T;
  let A such that
A1: A is finite-ind;
  func ind A -> Integer means
  :Def5:
  A in (Seq_of_ind T).(it+1) & not A in ( Seq_of_ind T).it;
  existence
  proof
    defpred P[Nat] means A in (Seq_of_ind T).$1;
A2: ex n st P[n] by A1;
    consider MIN be Nat such that
A3: P[MIN] and
A4: for n st P[n] holds MIN<=n from NAT_1:sch 5(A2);
    take I=MIN-1;
    now
      assume
A5:   A in (Seq_of_ind T).I;
      then I in dom(Seq_of_ind T) by FUNCT_1:def 2;
      then reconsider i=I as Element of NAT;
      MIN<=i by A4,A5;
      then MIN<i+1 by NAT_1:13;
      hence contradiction;
    end;
    hence thesis by A3;
  end;
  uniqueness
  proof
    let I1,I2 be Integer such that
A6: A in (Seq_of_ind T).(I1+1) and
A7: not A in (Seq_of_ind T).I1 and
A8: A in (Seq_of_ind T).(I2+1) and
A9: not A in (Seq_of_ind T).I2;
    I1+1 in dom(Seq_of_ind T) & I2+1 in dom(Seq_of_ind T) by A6,A8,
FUNCT_1:def 2;
    then reconsider i11=I1+1,i21=I2+1 as Element of NAT;
A10: I1<=I2
    proof
      assume I1>I2;
      then
A11:  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 A11,PROB_1:def 5;
      hence contradiction by A7,A8;
    end;
    I2<=I1
    proof
      assume I1<I2;
      then
A12:  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 A12,PROB_1:def 5;
      hence contradiction by A6,A9;
    end;
    hence thesis by A10,XXREAL_0:1;
  end;
end;

theorem Th5:
  -1 <= ind Af
proof
  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 thesis by A1,XREAL_1:6;
end;

theorem Th6:
  ind Af = -1 iff Af is empty
proof
  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
    assume ind Af=-1;
    then Af in (Seq_of_ind T).(-1+1) by Def5;
    hence Af is empty by A2,TARSKI:def 1;
  end;
  assume Af is empty;
  then
A3: Af in (Seq_of_ind T).0 by A2,TARSKI:def 1;
  -1+1=0;
  hence thesis by A1,A3,Def5;
end;

Lm3: ind Af+1 is Nat
proof
  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 thesis;
end;

registration
  let T be non empty TopSpace;
  let A be non empty finite-ind Subset of T;
  cluster ind A -> natural;
  coherence
  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 thesis;
  end;
end;

theorem Th7:
  ind Af <= n-1 iff Af in (Seq_of_ind T).n
proof
  set I=ind Af;
A1: Af in (Seq_of_ind T).(I+1) by Def5;
A2: I+1 is Nat by Lm3;
  hereby
    assume I<=n-1;
    then
A3: I+1<=n-1+1 by XREAL_1:6;
    I+1 in NAT & n in NAT by A2,ORDINAL1:def 12;
    then (Seq_of_ind T).(I+1)c=(Seq_of_ind T).n by A3,PROB_1:def 5;
    hence Af in (Seq_of_ind T).n by A1;
  end;
  assume
A4: Af in (Seq_of_ind T).n;
  assume I>n-1;
  then
A5: I>=n-1+1 by INT_1:7;
  then n in NAT & I in NAT by INT_1:3;
  then (Seq_of_ind T).n c=(Seq_of_ind T).I by A5,PROB_1:def 5;
  hence contradiction by A4,Def5;
end;

theorem
  for A be finite Subset of T holds ind A < card A
proof
  let A be finite Subset of T;
  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 thesis by A1,XXREAL_0:2;
end;

theorem Th9:
  ind Af <= n iff for p be Point of T|Af,U be open Subset of T|Af
st p in U ex W be open Subset of T|Af st p in W & W c= U & Fr W is finite-ind &
  ind Fr W <= n-1
proof
  set I=ind Af;
A1: [#](T|Af)c=[#]T by PRE_TOPC:def 4;
A2: Af in (Seq_of_ind T).(I+1) & not Af in (Seq_of_ind T).I by Def5;
  hereby
    assume
A3: I<=n;
    let p be Point of T|Af,U be open Subset of T|Af such that
A4: p in U;
    Af is non empty & T is non empty by A4;
    then reconsider I as Nat by TARSKI:1;
A5: I-1<=n-1 by A3,XREAL_1:9;
    consider W be 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;
A8: Fr W in (Seq_of_ind T|Af).I by A7,Th3;
    then Fr W is finite-ind;
    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,
XXREAL_0:2;
  end;
  assume
A9: for p be Point of T|Af,U be open Subset of T|Af st p in U ex W be
  open Subset of T|Af st p in W & W c=U & Fr W is finite-ind & ind Fr W <=n-1;
  now
    let p be Point of T|Af,U be open Subset of T|Af;
    assume p in U;
    then consider W be 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 be open Subset of T|Af st p in W & W c=U & Fr W in (Seq_of_ind T
    ).n by A10;
  end;
  then Af in (Seq_of_ind T).(n+1) by Def1;
  then ind Af<=n+1-1 by Th7;
  hence thesis;
end;

definition
  let T;
  let G such that
A1: G is finite-ind;
  func ind G -> Integer means
  :Def6:
  G c= (Seq_of_ind T).(it+1) & -1<=it & for
  i be Integer st-1<=i & G c= (Seq_of_ind T).(i+1) holds it<=i;
  existence
  proof
    defpred P[Nat] means G c=(Seq_of_ind T).$1;
A2: ex n st P[n] by A1;
    consider MIN be Nat such that
A3: P[MIN] and
A4: for n st P[n] holds MIN<=n from NAT_1:sch 5(A2);
    take I=MIN-1;
A5: now
      let i be Integer such that
A6:   -1<=i and
A7:   G c=(Seq_of_ind T).(i+1);
      -1+1<=i+1 by A6,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 A4,A7;
      hence I<=i by XREAL_1:6;
    end;
    I>=0-1 by XREAL_1:9;
    hence thesis by A3,A5;
  end;
  uniqueness
  proof
    let I1,I2 be Integer;
    assume G c=(Seq_of_ind T).(I1+1) & -1<=I1 & ( for i be 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 be Integer st-1<=i & G c=(Seq_of_ind T).(i+1) holds I2<=i );
    then I2<=I1 & I1<=I2;
    hence thesis by XXREAL_0:1;
  end;
end;

theorem
  ind G = -1 & G is finite-ind iff G c= {{}T}
proof
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;
  assume
A2: G c={{}T};
  then
A3: G is finite-ind by A1;
  then
A4: -1<=ind G by Def6;
  0=-1+1;
  then ind G<=-1 by A1,A2,A3,Def6;
  hence thesis by A1,A2,A4,XXREAL_0:1;
end;

theorem Th11:
  G is finite-ind & ind G <= I iff -1 <= I & for A st A in G holds
  A is finite-ind & ind A <= I
proof
  hereby
    assume that
A1: G is finite-ind and
A2: ind G<=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;
    let A such that
A4: A in G;
    thus A is finite-ind by A1,A4;
    then ind A<=iG-1 by A3,A4,Th7;
    hence ind A<=I by A2,XXREAL_0:2;
  end;
  assume that
A5: -1<=I and
A6: for A st A in G holds A is finite-ind & ind A<=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 object such that
A8: x in G;
    reconsider A=x as Subset of T by A8;
A9: I=I1-1;
    A is finite-ind & ind A<=I by A6,A8;
    hence thesis by A9,Th7;
  end;
  then G is finite-ind;
  hence thesis by A5,A7,Def6;
end;

theorem
  G1 is finite-ind & G2 c= G1 implies G2 is finite-ind & ind G2 <= ind G1
proof
  assume that
A1: G1 is finite-ind and
A2: G2 c=G1;
A3: -1<=ind G1 by A1,Th11;
  then for A st A in G2 holds A is finite-ind & ind A<=ind G1 by A1,A2,Th11;
  hence thesis by A3,Th11;
end;

Lm4: for i be 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 i be Integer such that
A1: G is finite-ind and
A2: G1 is finite-ind and
A3: ind G<=i and
A4: ind G1<=i;
A5: for A st A in G\/G1 holds A is finite-ind & ind A<=i
  proof
    let A;
    assume A in G\/G1;
    then A in G or A in G1 by XBOOLE_0:def 3;
    hence thesis by A1,A2,A3,A4,Th11;
  end;
  -1<=i by A1,A3,Th11;
  hence thesis by A5,Th11;
end;

registration
  let T;
  let G1,G2 be finite-ind Subset-Family of T;
  cluster G1 \/ G2 -> finite-ind for Subset-Family of T;
  coherence
  proof
    set iG1=ind G1+1,iG2=ind G2+1;
    -1<=ind G1 by Def6;
    then -1+1<=iG1 by XREAL_1:6;
    then
A1: iG1 in NAT by INT_1:3;
    -1<=ind G2 by Def6;
    then -1+1<=iG2 by XREAL_1:6;
    then
A2: iG2 in NAT by INT_1:3;
    then ind G1+0<=iG1 & iG1<=iG1+iG2 by A1,NAT_1:11,XREAL_1:6;
    then
A3: ind G1<=iG1+iG2 by XXREAL_0:2;
    ind G2+0<=iG2 & iG2<=iG2+iG1 by A2,A1,NAT_1:11,XREAL_1:6;
    then ind G2<=iG1+iG2 by XXREAL_0:2;
    hence thesis by A3,Lm4;
  end;
end;

theorem
  G is finite-ind & G1 is finite-ind & ind G <= I & ind G1 <= I implies
  ind (G\/G1) <= I by Lm4;

definition
  let T;
  func ind T -> Integer equals
  ind [#]T;
  correctness;
end;

registration
  let T be non empty finite-ind TopSpace;
  cluster ind T -> natural;
  coherence
  proof
    [#]T is non empty finite-ind by Def4;
    hence thesis;
  end;
end;

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

theorem Th15:
  (ex n st for p be Point of T,U be open Subset of T st p in U ex
W be 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
proof
  given n such that
A1: for p be Point of T,U be open Subset of T st p in U ex W be open
  Subset of T st p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1;
  set CT=[#]T;
  set TT=T|CT;
A2: [#]TT=CT by PRE_TOPC:def 5;
  T is SubSpace of T by TSEP_1:2;
  then
A3: the TopStruct of T=the TopStruct of TT by A2,TSEP_1:5;
  now
    let p9 be Point of TT,U9 be open Subset of TT such that
A4: p9 in U9;
    reconsider p=p9 as Point of T by A2;
    U9 in the topology of TT by PRE_TOPC:def 2;
    then reconsider U=U9 as open Subset of T by A3,PRE_TOPC:def 2;
    consider W be 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 TT by A3,PRE_TOPC:def 2;
    take W9;
    T is non 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;
  end;
  then CT in (Seq_of_ind T).(n+1) by Def1;
  then CT is finite-ind;
  hence thesis;
end;

theorem Th16:
  ind Tf <= n iff for p be Point of Tf,U be open Subset of Tf st p
in U ex W be open Subset of Tf st p in W & W c= U & Fr W is finite-ind & ind Fr
  W <= n-1
proof
  set CT=[#]Tf;
  set TT=Tf|CT;
A1: [#]TT=CT by PRE_TOPC:def 5;
  Tf is SubSpace of Tf by TSEP_1:2;
  then
A2: the TopStruct of Tf=the TopStruct of TT by A1,TSEP_1:5;
A3: CT is finite-ind by Def4;
  hereby
    assume
A4: ind Tf<=n;
    let p be Point of Tf,U be open Subset of Tf such that
A5: p in U;
    reconsider p9=p as Point of TT by A1;
    U in the topology of Tf by PRE_TOPC:def 2;
    then reconsider U9=U as open Subset of TT by A2,PRE_TOPC:def 2;
    consider W9 be open Subset of TT 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 TT by PRE_TOPC:def 2;
    then reconsider W=W9 as open Subset of Tf by A2,PRE_TOPC:def 2;
    Tf is non 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;
    Fr W9 in (Seq_of_ind TT).n by A7,Th7;
    then
A9: Fr W in (Seq_of_ind Tf).n by A8,Th3;
    then Fr W is finite-ind;
    hence p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1 by A6,A9,Th7;
  end;
  assume
A10: for p be Point of Tf,U be open Subset of Tf st p in U ex W be open
  Subset of Tf st p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1;
  now
    let p9 be Point of TT,U9 be open Subset of TT such that
A11: p9 in U9;
    reconsider p=p9 as Point of Tf by A1;
    U9 in the topology of TT by PRE_TOPC:def 2;
    then reconsider U=U9 as open Subset of Tf by A2,PRE_TOPC:def 2;
    consider W be 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 TT by A2,PRE_TOPC:def 2;
    Tf is non 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;
    Fr W in (Seq_of_ind Tf).n by A13,Th7;
    then
A15: Fr W9 in (Seq_of_ind TT).n by A14,Th3;
    then Fr W9 is finite-ind;
    hence
    p9 in W9 & W9 c=U9 & Fr W9 is finite-ind & ind Fr W9<=n-1 by A12,A15,Th7;
  end;
  hence thesis by A3,Th9;
end;

Lm5: T|Af is finite-ind & ind T|Af = ind Af
proof
  set TA=T|Af;
A1: [#]TA=Af by PRE_TOPC:def 5;
  per cases by Th6;
  suppose
A2: ind Af=-1;
    then Af={}T by Th6;
    hence thesis by A2,Th6;
  end;
  suppose
A3: Af is non empty;
    then T is non empty;
    then reconsider n=ind Af as Nat by A3,TARSKI:1;
    Af in (Seq_of_ind T).(n+1) by Def5;
    then
A4: [#]TA in (Seq_of_ind TA).(n+1) by A1,Th3;
    then
A5: [#]TA is finite-ind;
    hence TA is finite-ind;
A6: ind[#]TA>=n
    proof
      assume ind[#]TA<n;
      then ind[#]TA+1<=n by INT_1:7;
      then ind[#]TA+1-1<=n-1 by XREAL_1:9;
      then [#]TA in (Seq_of_ind TA).n by A5,Th7;
      then Af in (Seq_of_ind T).n by A1,Th3;
      hence thesis by Def5;
    end;
    ind[#]TA<=n+1-1 by A4,A5,Th7;
    hence ind TA=ind Af by A6,XXREAL_0:1;
  end;
end;

Lm6: for A be Subset of Tf holds Tf|A is finite-ind & ind Tf|A <= ind Tf
proof
  defpred P[Nat] means for T st T is finite-ind & ind T=$1-1 for A be 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 be Nat st for n st n<k holds P[n] holds P[k]
  proof
    let n9 be Nat such that
A2: for n st n<n9 holds P[n];
    per cases;
    suppose
A3:   n9=0;
      let T such that
A4:   T is finite-ind and
A5:   ind T=n9-1;
      let A be Subset of T;
      [#]T is finite-ind by A4;
      then [#]T={}T by A3,A5,Th6;
      hence thesis by A3,A5,Th6;
    end;
    suppose
      n9>0;
      then reconsider n=n9-1 as Nat by NAT_1:20;
      let T such that
A6:   T is finite-ind and
A7:   ind T=n9-1;
      let A be Subset of T;
      set TA=T|A;
A8:   [#]TA=A by PRE_TOPC:def 5;
A9:   now
        let p be Point of TA,U be open Subset of TA such that
A10:    p in U;
        U in the topology of TA by PRE_TOPC:def 2;
        then consider U9 be Subset of T such that
A11:    U9 in the topology of T and
A12:    U=U9/\[#]TA 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 be 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,10;
        then ind Fr W9+1<n9 by XXREAL_0:2;
        then
A17:    P[i] by A2;
        reconsider W=W9/\[#]TA as Subset of TA;
        W9 in the topology of T by PRE_TOPC:def 2;
        then W in the topology of TA by PRE_TOPC:def 4;
        then reconsider W as open Subset of TA by PRE_TOPC:def 2;
        set FR9=Fr W9;
        set TF=T|FR9;
        [#]TF=FR9 & Fr W c=Fr W9/\A by A8,Th1,PRE_TOPC:def 5;
        then reconsider FrW=Fr W as Subset of TF by XBOOLE_1:18;
        take W;
        [#]TF c=[#]T by PRE_TOPC:def 4;
        then reconsider FrW9=FrW as Subset of T by XBOOLE_1:1;
A18:    TF is finite-ind & ind TF=ind FR9 by A15,Lm5;
        then TF|FrW is finite-ind by A17;
        then
A19:    [#](TF|FrW) is finite-ind;
        ind(TF|FrW)<=ind FR9 by A17,A18;
        then ind[#](TF|FrW)<=n-1 by A16,XXREAL_0:2;
        then [#](TF|FrW)=FrW & [#](TF|FrW) in (Seq_of_ind(TF|FrW)).n by A19,Th7
,PRE_TOPC:def 5;
        then FrW in (Seq_of_ind TF).n by Th3;
        then FrW9 in (Seq_of_ind T).n by Th3;
        then
A20:    Fr W in (Seq_of_ind TA).n by Th3;
        then Fr W is finite-ind;
        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;
      end;
      then TA is finite-ind by Th15;
      hence thesis by A7,A9,Th16;
    end;
  end;
  for n holds P[n] from NAT_1:sch 4(A1);
  then P[i];
  hence thesis;
end;

Lm7: T is finite-ind implies A is finite-ind
proof
  set TA=T|A;
  assume T is finite-ind;
  then TA is finite-ind by Lm6;
  then [#]TA is finite-ind;
  then consider n such that
A1: [#]TA in (Seq_of_ind TA).n;
  [#]TA=A by PRE_TOPC:def 5;
  then A in (Seq_of_ind T).n by A1,Th3;
  hence thesis;
end;

begin :: Monotonic of the Small Inductive Dimension

registration
  let Tf;
  cluster -> finite-ind for Subset of Tf;
  coherence by Lm7;
end;

registration
  let T,Af;
  cluster T|Af -> finite-ind;
  coherence by Lm5;
end;

::  Teoria wymiaru Th 1.1.2

theorem
  ind T|Af = ind Af by Lm5;

theorem Th18:
  T|A is finite-ind implies A is finite-ind
proof
  assume T|A is finite-ind;
  then consider n 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 thesis;
end;

theorem Th19:
  A c= Af implies A is finite-ind & ind A <= ind Af
proof
  assume
A1: A c=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;
  then ind T|A=ind A by Lm5;
  hence thesis by A2,A3,Lm6;
end;

theorem
  for A be Subset of Tf holds ind A <= ind Tf by Th19;

theorem Th21:
  F = B & B is finite-ind implies F is finite-ind & ind F = ind B
proof
  assume that
A1: F=B and
A2: B is finite-ind;
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 thesis by A2,A3,Th18;
end;

theorem Th22:
  F = B & F is finite-ind implies B is finite-ind & ind F = ind B
proof
  assume that
A1: F=B and
A2: F is finite-ind;
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 thesis by A2,A3,Th18;
end;

Lm8: for T1,T2 be TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds
T2 is finite-ind & ind T2<=ind T1
proof
  defpred P[Nat] means for T1,T2 be 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 such that
A1: T1,T2 are_homeomorphic and
A2: T1 is finite-ind;
  reconsider i=ind T1+1 as Nat by A2,Lm3;
A3: for n st P[n] holds P[n+1]
  proof
    let n such that
A4: P[n];
    set n1=n+1;
    let T1,T2 be TopSpace such that
A5: T1,T2 are_homeomorphic and
A6: T1 is finite-ind and
A7: ind T1<=n+1;
    consider f be 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;
A10: rng f=[#]T2 by A8;
A11:  f is onto by A10;
A12: f is one-to-one by A8;
    per cases;
    suppose
A13:  [#]T1={}T1;
      then ind T1=-1 by Th6;
      hence thesis by A10,A13,Th6;
    end;
    suppose
A14:  [#]T1<>{}T1;
      then T1 is non empty;
      then reconsider i=ind T1 as Nat by A6,TARSKI:1;
A15:  T1 is non empty by A14;
A16:  T2 is non empty by A9,A14;
      per cases by A7,NAT_1:8;
      suppose
        i<=n;
        hence thesis by A4,A5,A6;
      end;
      suppose
A17:    ind T1=n+1;
A18:    dom f9=[#]T2 by A10,A12,A16,TOPS_2:49;
A19:    for p be Point of T2,U be open Subset of T2 st p in U ex W be
open Subset of T2 st p in W & W c=U & Fr W is finite-ind & ind Fr W<=n1-1
        proof
          reconsider F=f as Function;
          let p be Point of T2,U be open Subset of T2;
          assume p in U;
          then
A20:      f9.p in f9.:U by A18,FUNCT_1:def 6;
          f"U=f9.:U & f"U is open by A8,A15,A16,TOPGRP_1:26,TOPS_2:55;
          then consider W be open Subset of T1 such that
A21:      f9.p in W and
A22:      W c=f"U and
A23:      Fr W is finite-ind and
A24:      ind Fr W<=n1-1 by A6,A17,A20,Th16;
          set FW=Fr W;
A25:      ind(T1|FW)=ind FW by A23,Lm5;
          FW,f.:FW are_homeomorphic by A8,METRIZTS:3;
          then
A26:      T1|FW,T2|(f.:FW)are_homeomorphic by METRIZTS:def 1;
          then T2|(f.:FW) is finite-ind by A4,A23,A24,A25;
          then
A27:      f.:FW is finite-ind by Th18;
          F"=f9 by A11,A12,TOPS_2:def 4;
          then
A28:      f.(f9.p)=p by A10,A12,A16,FUNCT_1:35;
          ind(T2|(f.:FW))<=ind(T1|FW) by A4,A23,A24,A25,A26;
          then
A29:      ind(T2|(f.:FW))<=n1-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;
          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,def 6;
          f.:FW=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 thesis by A27,A29,Lm5;
        end;
        then T2 is finite-ind by Th15;
        hence thesis by A17,A19,Th16;
      end;
    end;
  end;
A30: P[0]
  proof
    let T1,T2 be TopSpace such that
A31: T1,T2 are_homeomorphic and
A32: T1 is finite-ind and
A33: ind T1<=0;
    consider f be 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;
A36: rng f=[#]T2 by A34;
A37:  f is onto by A36;
A38: f is one-to-one by A34;
    per cases;
    suppose
A39:  [#]T1={}T1;
      then ind T1=-1 by Th6;
      hence thesis by A36,A39,Th6;
    end;
    suppose
A40:  [#]T1<>{}T1;
      then T1 is non empty;
      then reconsider i=ind T1 as Nat by A32,TARSKI:1;
A41:  i=0 by A33;
A42:  T1 is non empty by A40;
A43:  T2 is non empty by A35,A40;
      then
A44:  dom f9=[#]T2 by A36,A38,TOPS_2:49;
A45:  for p be Point of T2,U be open Subset of T2 st p in U ex W be 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,U be open Subset of T2;
        assume p in U;
        then
A46:    f9.p in f9.:U by A44,FUNCT_1:def 6;
        F"=f9 by A37,A38,TOPS_2:def 4;
        then
A47:    f.(f9.p)=p by A36,A38,A43,FUNCT_1:35;
        f"U=f9.:U & f"U is open by A34,A42,A43,TOPGRP_1:26,TOPS_2:55;
        then consider W be open Subset of T1 such that
A48:    f9.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;
        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,def 6;
        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 thesis by Th6;
      end;
      then T2 is finite-ind by Th15;
      hence thesis by A41,A45,Th16;
    end;
  end;
A52: for n holds P[n] from NAT_1:sch 2(A30,A3);
  ind T1+0<=i by XREAL_1:6;
  hence thesis by A1,A2,A52;
end;

Lm9: for T1,T2 be TopSpace st T1,T2 are_homeomorphic holds(T1 is finite-ind
iff T2 is finite-ind) & (T1 is finite-ind implies ind T2=ind T1)
proof
  let T1,T2 be TopSpace such that
A1: T1,T2 are_homeomorphic;
  consider f be Function of T1,T2 such that
A2: f is being_homeomorphism by A1,T_0TOPSP:def 1;
A3: dom f=[#]T1 by A2;
A4: rng f=[#]T2 by A2;
  per cases;
  suppose
A5: [#]T1={}T1;
    then ind[#]T2=-1 by A4,Th6;
    hence thesis by A4,A5,Th6;
  end;
  suppose
    T1 is non empty;
    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;
    assume
A7: T1 is finite-ind;
    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 thesis by A8,XXREAL_0:1;
  end;
end;

::  Teoria wymiaru Th 1.1.4

theorem
  for T be non empty TopSpace st T is regular holds T is finite-ind &
  ind T <= n iff for A be closed Subset of T,p be Point of T st not p in A ex L
  be Subset of T st L separates{p},A & L is finite-ind & ind L <= n-1
proof
  let T be non empty TopSpace such that
A1: T is regular;
  hereby
    assume
A2: T is finite-ind & ind T<=n;
    let A be closed Subset of T,p be Point of T;
    assume not p in A;
    then p in A` by XBOOLE_0:def 5;
    then consider V1,V2 be 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 be 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;
A12: L =(Cl W1\W1)`` by TOPS_1:42
      .=(([#]T\Cl W1)\/[#]T/\W1)` by XBOOLE_1:52
      .=((Cl W1)`\/W1)` by XBOOLE_1:28;
    V2 misses Cl V1 by A4,A7,TSEP_1:36;
    then
A13: Cl V1 c=V2` by SUBSET_1:23;
    Cl W1 c=Cl V1 by A10,PRE_TOPC:19;
    then Cl W1 c=V2` by A13;
    then Cl W1 c=A` by A8;
    then
A14: A c=(Cl W1)` by SUBSET_1:16;
    W1 c=Cl W1 by PRE_TOPC:18;
    then
A15: (Cl W1)`misses W1 by SUBSET_1:24;
    {p}c=W1 by A9,ZFMISC_1:31;
    hence L separates{p},A & L is finite-ind & ind L<=n-1 by A11,A12,A14,A15,
METRIZTS:def 3;
  end;
  assume
A16: for A be closed Subset of T,p be Point of T st not p in A ex L be
  Subset of T st L separates{p},A & L is finite-ind & ind L<=n-1;
A17: for p be Point of T,U be open Subset of T st p in U ex W be 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,U be open Subset of T;
    assume p in U;
    then not p in U` by XBOOLE_0:def 5;
    then consider L be 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 be 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,23;
    take A1;
    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 thesis by A19,A20,A21,A25,A26,Th19,XXREAL_0:2,ZFMISC_1:31;
  end;
  then T is finite-ind by Th15;
  hence thesis by A17,Th16;
end;

theorem
  T1,T2 are_homeomorphic implies (T1 is finite-ind iff T2 is finite-ind)
  by Lm9;

theorem
  T1,T2 are_homeomorphic & T1 is finite-ind implies ind T1 = ind T2 by Lm9;

theorem Th26:
  for A1 be Subset of T1,A2 be Subset of T2 st A1,A2
  are_homeomorphic holds A1 is finite-ind iff A2 is finite-ind
proof
  let A1 be Subset of T1,A2 be Subset of T2;
  assume A1,A2 are_homeomorphic;
  then
A1: T1|A1,T2|A2 are_homeomorphic by METRIZTS:def 1;
  hereby
    assume A1 is finite-ind;
    then T2|A2 is finite-ind by A1,Lm9;
    hence A2 is finite-ind by Th18;
  end;
  assume A2 is finite-ind;
  then T1|A1 is finite-ind by A1,Lm9;
  hence thesis by Th18;
end;

theorem
  for A1 be Subset of T1,A2 be Subset of T2 st A1,A2 are_homeomorphic &
  A1 is finite-ind holds ind A1 = ind A2
proof
  let A1 be Subset of T1,A2 be Subset of T2 such that
A1: A1,A2 are_homeomorphic and
A2: A1 is finite-ind;
  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 thesis by A3,Lm5;
end;

theorem
  [:T1,T2:] is finite-ind implies [:T2,T1:] is finite-ind & ind [:T1,T2
  :] = ind [:T2,T1:]
proof
  assume
A1: [:T1,T2:] is finite-ind;
  per cases;
  suppose
A2: T1 is empty or T2 is empty;
    then ind[:T1,T2:]=-1 by Th6;
    hence thesis by A2,Th6;
  end;
  suppose
    T1 is non empty & T2 is non empty;
    then [:T1,T2:],[:T2,T1:]are_homeomorphic by YELLOW12:44;
    hence thesis by A1,Lm9;
  end;
end;

theorem
  for Ga be Subset-Family of T|A st Ga is finite-ind & Ga = G holds G is
  finite-ind & ind G = ind Ga
proof
  let G1 be Subset-Family of T|A such that
A1: G1 is finite-ind and
A2: G1=G;
A3: for B be Subset of T st B in G holds B is finite-ind & ind B<= ind G1
  proof
    let B be Subset of T;
    assume
A4: B in G;
    then reconsider B9=B as Subset of T|A by A2;
A5: B9 is finite-ind by A1,A2,A4;
    then ind B=ind B9 by Th22;
    hence thesis by A1,A2,A4,A5,Th11,Th22;
  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 be 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;
    assume
A10: B in G1;
    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 thesis by A1,A2,A8,A10,Th11;
  end;
  -1<=ind G by A8,Th11;
  then ind G1<=ind G by A9,Th11;
  hence thesis by A3,A6,A7,Th11,XXREAL_0:1;
end;

theorem
  for Ga be Subset-Family of T|A st G is finite-ind & Ga = G holds Ga is
  finite-ind & ind G = ind Ga
proof
  let G1 be Subset-Family of T|A such that
A1: G is finite-ind and
A2: G1=G;
A3: for B be 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;
    assume
A4: B in G1;
    then reconsider B9=B as Subset of T by A2;
A5: B9 is finite-ind by A1,A2,A4;
    then ind B=ind B9 by Th21;
    hence thesis by A1,A2,A4,A5,Th11,Th21;
  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 be Subset of T st B in G holds B is finite-ind & ind B<= ind G1
  proof
    let B be Subset of T;
    assume
A10: B in G;
    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 thesis by A1,A2,A8,A10,Th11;
  end;
  -1<=ind G1 by A8,Th11;
  then ind G<=ind G1 by A9,Th11;
  hence thesis by A3,A6,A7,Th11,XXREAL_0:1;
end;

begin :: Basic Properties for zero dimensional Topological Spaces
::  Teoria wymiaru Th 1.1.6

theorem Th31:
  T is finite-ind & ind T <= n iff ex Bas be Basis of T st for A
  st A in Bas holds Fr A is finite-ind & ind Fr A <= n-1
proof
  set TOP=the topology of T;
  set cT=the carrier of T;
  hereby
    defpred P[object,object] means
    for p be Point of T,A be Subset of T st$1=[p,A]
    holds$2 in TOP & (not p in A implies $2={}T) & (p in A implies ex W be 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;
A3: for x be object st x in [:cT,TOP:]ex y be object st P[x,y]
    proof
      let x be object;
      assume x in [:cT,TOP:];
      then consider p9,A9 be object such that
A4:   p9 in cT and
A5:   A9 in TOP and
A6:   x=[p9,A9] by ZFMISC_1:def 2;
      reconsider p9 as Point of T by A4;
      reconsider A9 as open Subset of T by A5,PRE_TOPC:def 2;
      per cases;
      suppose
A7:     not p9 in A9;
        take{}T;
        let p be Point of T,A such that
A8:     x=[p,A];
        p=p9 by A6,A8,XTUPLE_0:1;
        hence thesis by A6,A7,A8,PRE_TOPC:def 2,XTUPLE_0:1;
      end;
      suppose
        p9 in A9;
        then consider W be 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;
        let p be Point of T,A;
        assume x=[p,A];
        then p=p9 & A=A9 by A6,XTUPLE_0:1;
        hence thesis by A9,A10,PRE_TOPC:def 2;
      end;
    end;
    consider f be Function such that
A11: dom f=[:cT,TOP:] and
A12: for x be object st x in [:cT,TOP:] holds P[x,f.x]
    from CLASSES1:sch
    1(A3);
A13: rng f c=TOP
    proof
      let y be object;
      assume y in rng f;
      then consider x be object such that
A14:  x in dom f and
A15:  f.x=y by FUNCT_1:def 3;
      ex p,A be object st p in cT & A in TOP & x=[p,A]
by A11,A14,ZFMISC_1:def 2;
      hence thesis by A11,A12,A14,A15;
    end;
    then reconsider RNG=rng f as Subset-Family of T by XBOOLE_1:1;
    now
      let A be Subset of T;
      assume A is open;
      then
A16:  A in TOP by PRE_TOPC:def 2;
      let p be Point of T such that
A17:  p in A;
A18:  [p,A] in [:cT,TOP:] by A16,A17,ZFMISC_1:87;
      then consider W be 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 as Subset of T;
      take W;
      thus W in RNG & p in W & W c=A by A11,A18,A19,FUNCT_1:def 3;
    end;
    then reconsider RNG as Basis of T by A13,YELLOW_9:32;
    take RNG;
    let B be Subset of T;
    assume B in RNG;
    then consider x be object such that
A20: x in dom f and
A21: f.x=B by FUNCT_1:def 3;
    consider p,A be object such that
A22: p in cT and
A23: A in TOP and
A24: x=[p,A] by A11,A20,ZFMISC_1:def 2;
    reconsider A as set by TARSKI:1;
    per cases;
    suppose
      p in A;
      then
      ex W be 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;
    end;
    suppose
A25:  not p in A;
A26:  T is non 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;
    end;
  end;
  given B be Basis of T such that
A28: for A be Subset of T st A in B holds Fr A is finite-ind & ind Fr A <=n-1;
A29: now
    let p be Point of T,U be open Subset of T;
    assume p in U;
    then consider W be Subset of T such that
A30: W in B and
A31: p in W & W c=U by YELLOW_9:31;
    B c=TOP by TOPS_2:64;
    then reconsider W as open Subset of T by A30,PRE_TOPC:def 2;
    take W;
    thus p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1 by A28,A30,A31;
  end;
  then T is finite-ind by Th15;
  hence thesis by A29,Th16;
end;

::  Wprowadzenie do topologi 3.4.2 "=>"

theorem Th32:
  for T st T is T_1 & for A,B be closed Subset of T st A misses B
ex A9,B9 be 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 such that
A1: T is T_1 & for A,B be closed Subset of T st A misses B ex A9,B9 be
  closed Subset of T st A9 misses B9 & A9\/B9=[#]T & A c=A9 & B c=B9;
A2: now
    let p be Point of T,U be open Subset of T such that
A3: p in U;
    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;
    T is non empty by A3;
    then consider A9,B9 be 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;
    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;
    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;
  end;
  then T is finite-ind by Th15;
  hence thesis by A2,Th16;
end;

theorem Th33:
  for X be set,f be SetSequence of X ex g be SetSequence of X st
union rng f = union rng g & (for i,j be Nat st i<>j holds g.i misses g.j) & for
n ex fn be 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,f be SetSequence of X;
  defpred P[object,object] means
   for n st n=$1ex fn be 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 be object st x in NAT ex y be object st y in bool X & P[x,y]
  proof
    let x be object;
    assume x in NAT;
    then reconsider n=x as Element of NAT;
    deffunc F(Nat)=f.$1;
    set fn={F(i) where i is Element of NAT:i in n};
A2: fn c=bool X
    proof
      let z be object;
      assume z in fn;
      then ex i be Element of NAT st z=F(i) & i in n;
      hence thesis;
    end;
A3: n is finite;
    fn is finite from FRAENKEL:sch 21(A3);
    then reconsider fn as finite Subset-Family of X by A2;
    take y=f.n\union fn;
    thus y in bool X;
    let m be Nat such that
A4: m=x;
    set Fn={f.i where i is Element of NAT:i<n};
    take fn;
A5: fn c=Fn
    proof
      let z be object;
      assume z in fn;
      then consider i be Element of NAT such that
A6:   z=f.i and
A7:   i in Segm n;
      i<n by A7,NAT_1:44;
      hence thesis by A6;
    end;
    Fn c=fn
    proof
      let z be object;
      assume z in Fn;
      then consider i be Element of NAT such that
A8:   z=f.i and
A9:   i<n;
      i in Segm n by A9,NAT_1:44;
      hence thesis by A8;
    end;
    hence thesis by A4,A5;
  end;
  consider g be SetSequence of X such that
A10: for x be object st x in NAT holds P[x,g.x] from FUNCT_2:sch 1(A1);
  take g;
A11: union rng f c=union rng g
  proof
    let y be object;
    defpred Q[Nat] means y in f.$1;
    assume y in union rng f;
    then consider Y be set such that
A12: y in Y and
A13: Y in rng f by TARSKI:def 4;
    ex x be object st x in dom f & f.x=Y by A13,FUNCT_1:def 3;
    then
A14: ex n st Q[n] by A12;
    consider Min be Nat such that
A15: Q[Min] and
A16: for n st Q[n] holds Min<=n from NAT_1:sch 5(A14);
A17: Min in NAT by ORDINAL1:def 12;
    then consider fn be 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;
      then consider Z be set such that
A20:  y in Z and
A21:  Z in fn by TARSKI:def 4;
      ex i be Element of NAT st Z=f.i & i<Min by A18,A21;
      hence thesis by A16,A20;
    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 thesis by A22,TARSKI:def 4;
  end;
  union rng g c=union rng f
  proof
    let y be object;
    assume y in union rng g;
    then consider Y be set such that
A23: y in Y and
A24: Y in rng g by TARSKI:def 4;
    consider x be object 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 be 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 thesis by A27,TARSKI:def 4;
  end;
  hence union rng f=union rng g by A11;
A28: for i,j be Nat st i<j holds g.i misses g.j
  proof
    let i,j be Nat such that
A29: i<j;
    j in NAT by ORDINAL1:def 12;
    then consider fj be 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;
    then consider x be object 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 be 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;
  end;
  thus for i,j be Nat st i<>j holds g.i misses g.j
  proof
    let i,j be Nat;
    assume i<>j;
    then i<j or j<i by XXREAL_0:1;
    hence thesis by A28;
  end;
  let n;
  n in NAT by ORDINAL1:def 12;
  hence thesis by A10;
end;

::  Wprowadzenie do topologi 3.4.2 "<="

theorem Th34:
  for T st T is finite-ind & ind T<=0 & T is Lindelof for A,B be
closed Subset of T st A misses B ex A9,B9 be closed Subset of T st A9 misses B9
  & A9\/B9 = [#]T & A c= A9 & B c= B9
proof
  let T such that
A1: T is finite-ind & ind T<=0 and
A2: T is Lindelof;
  set CT=[#]T;
  let A,B be closed Subset of T such that
A3: A misses B;
  per cases;
  suppose
A4: CT={};
    take A,B;
    thus thesis by A3,A4;
  end;
  suppose
A5: CT<>{};
    defpred P[object,object] means
     ex D2 being set st D2 = $2 &
     $1 is Point of T & $1 in D2 & $2 is open closed
      Subset of T & (D2 c=A` or D2 c=B`);
A6: for x be object st x in CT ex y be object st y in bool CT & P[x,y]
    proof
      let x be object such that
A7:   x in CT;
      reconsider p=x as Point of T by A7;
      per cases;
      suppose
        p in A`;
        then consider W be 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;
        thus W in bool CT;
        take W;
        thus W = 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 thesis by A8,TOPGEN_1:14;
      end;
      suppose
A11:    not p in A`;
A12:    A c=B` by A3,SUBSET_1:23;
        p in A by A7,A11,XBOOLE_0:def 5;
        then consider W be 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;
        thus W in bool CT;
        take 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 thesis by A13,TOPGEN_1:14;
      end;
    end;
    consider F be Function of CT,bool CT such that
A16: for x be object st x in CT holds P[x,F.x] from FUNCT_2:sch 1(A6);
    reconsider RNG=rng F as Subset-Family of T;
A17: dom F=CT by FUNCT_2:def 1;
    CT c=union RNG
    proof
      let x be object such that
A18:  x in CT;
      reconsider p=x as Point of T by A18;
      P[x,F.x] by A16,A18;
      then p in F.p & F.p in RNG by A17,FUNCT_1:def 3;
      hence thesis by TARSKI:def 4;
    end;
    then [#]T=union RNG;
    then
A19: RNG is Cover of T by SETFAM_1:45;
    RNG is open
    proof
      let U be Subset of T;
      assume U in RNG;
      then consider x be object such that
A20:     x in dom F & F.x=U by FUNCT_1:def 3;
       P[x,U] by A20,A16;
      hence thesis;
    end;
    then consider G be Subset-Family of T such that
A21: G c=RNG and
A22: G is Cover of T and
A23: G is countable by A2,A19,METRIZTS:def 2;
    T is non empty by A5;
    then
A24: G is non empty by A22,TOPS_2:3;
    then consider U be sequence of G such that
A25: rng U=G by A23,CARD_3:96;
A26: dom U=NAT by A24,FUNCT_2:def 1;
    then reconsider U as SetSequence of CT by A25,FUNCT_2:2;
    consider V be SetSequence of CT such that
A27: union rng U=union rng V and
A28: for i,j be Nat st i<>j holds V.i misses V.j and
A29: for n ex Un be finite Subset-Family of CT 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};
A30: AA c=rng V
    proof
      let x be object;
      assume x in AA;
      then dom V=NAT & ex n be Element of NAT st x=V.n & V.n misses B by
FUNCT_2:def 1;
      hence thesis by FUNCT_1:def 3;
    end;
    then reconsider AA as Subset-Family of T by XBOOLE_1:1;
    set BB=rngV\AA;
A31: rngV is open
    proof
      let A be Subset of T;
      assume A in rngV;
      then consider m be object such that
A32:  m in dom V and
A33:  V.m=A by FUNCT_1:def 3;
      reconsider m as Element of NAT by A32;
      consider Un be finite Subset-Family of CT such that
A34:  Un={U.i where i is Element of NAT:i<m} and
A35:  V.m=U.m\union Un by A29;
      reconsider Un as Subset-Family of T;
      U.m in rng U by A26,FUNCT_1:def 3;
      then consider x be object such that
A36:     x in dom F & F.x=U.m by A21,A25,FUNCT_1:def 3;
      P[x,U.m] by A36,A16;
      then reconsider UN=U.m as open Subset of T;
      Un is closed
      proof
        let D be Subset of T;
        assume D in Un;
        then ex i be Element of NAT st D=U.i & i<m by A34;
        then D in rng U by A26,FUNCT_1:def 3;
        then consider x be object such that
A37:  x in dom F & F.x=D by A21,A25,FUNCT_1:def 3;
         P[x,D] by A37,A16;
        hence thesis;
      end;
      then union Un is closed by TOPS_2:21;
      then UN/\(union Un)` is open;
      hence thesis by A33,A35,SUBSET_1:13;
    end;
    then union AA is open by A30,TOPS_2:11,19;
    then reconsider UAA=union AA,UBB=union BB as open Subset of T by A31,
TOPS_2:15,19;
A38: UAA misses UBB
    proof
      assume UAA meets UBB;
      then consider x be object such that
A39:  x in union AA and
A40:  x in union BB by XBOOLE_0:3;
      consider Ax be set such that
A41:  x in Ax and
A42:  Ax in AA by A39,TARSKI:def 4;
      consider n be Element of NAT such that
A43:  V.n=Ax and
A44:  V.n misses B by A42;
      consider Bx be set such that
A45:  x in Bx and
A46:  Bx in BB by A40,TARSKI:def 4;
      Bx in rngV by A46,XBOOLE_0:def 5;
      then consider m be object such that
A47:  m in dom V and
A48:  V.m=Bx by FUNCT_1:def 3;
      reconsider m as Element of NAT by A47;
      not Bx in AA by A46,XBOOLE_0:def 5;
      then m<>n by A44,A48;
      then V.n misses V.m by A28;
      hence thesis by A41,A43,A45,A48,XBOOLE_0:3;
    end;
    rngV=BB\/AA by A30,XBOOLE_1:45;
    then
A49: UAA\/UBB=union G by A25,A27,ZFMISC_1:78
      .=[#]T by A22,SETFAM_1:45;
    then
A50: UAA=UBB` by A38,PRE_TOPC:5;
    B misses UAA
    proof
      assume B meets UAA;
      then consider x be object such that
A51:  x in B and
A52:  x in union AA by XBOOLE_0:3;
      consider Ax be set such that
A53:  x in Ax and
A54:  Ax in AA by A52,TARSKI:def 4;
      ex n be Element of NAT st V.n=Ax & V.n misses B by A54;
      hence thesis by A51,A53,XBOOLE_0:3;
    end;
    then
A55: B c=UAA` by SUBSET_1:23;
    A misses UBB
    proof
      assume A meets UBB;
      then consider x be object such that
A56:  x in A and
A57:  x in union BB by XBOOLE_0:3;
      consider Bx be set such that
A58:  x in Bx and
A59:  Bx in BB by A57,TARSKI:def 4;
      Bx in rngV by A59,XBOOLE_0:def 5;
      then consider m be object such that
A60:  m in dom V and
A61:  V.m=Bx by FUNCT_1:def 3;
      reconsider m as Element of NAT by A60;
      not V.m in AA by A59,A61,XBOOLE_0:def 5;
      then V.m meets B;
      then consider b be object such that
A62:  b in V.m and
A63:  b in B by XBOOLE_0:3;
      U.m in rng U by A26,FUNCT_1:def 3;
      then consider p be object such that
A64:  p in dom F and
A65:  F.p=U.m by A21,A25,FUNCT_1:def 3;
      reconsider Fp=F.p as Subset of T by A65;
A66:  ex Un be finite Subset of bool CT st Un={U.i where i is Element of
      NAT:i<m} & V.m=U.m\union Un by A29;
      then b in U.m by A62,XBOOLE_0:def 5;
      then Fp meets B by A63,A65,XBOOLE_0:3;
      then
A67:     not Fp c=B` by SUBSET_1:23;
      P[p,F.p] by A16,A64;
      then
A68:  U.m c=A` by A65,A67;
      x in U.m by A58,A61,A66,XBOOLE_0:def 5;
      hence thesis by A56,A68,XBOOLE_0:def 5;
    end;
    then A c=UAA by A50,SUBSET_1:23;
    hence thesis by A38,A49,A50,A55;
  end;
end;

::  Teoria wymiaru Th 1.2.6

theorem Th35:
  for T st T is T_1 & T is Lindelof holds T is finite-ind & ind T
  <= 0 iff for A,B be closed Subset of T st A misses B holds {}T separates A,B
proof
  let T such that
A1: T is T_1 and
A2: T is Lindelof;
  hereby
    assume
A3: T is finite-ind & ind T<=0;
    let A,B be closed Subset of T;
    assume A misses B;
    then consider A9,B9 be 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;
  end;
  assume
A8: for A,B be closed Subset of T st A misses B holds{}T separates A,B;
  for A,B be closed Subset of T st A misses B ex A9,B9 be 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;
    assume A misses B;
    then {}T separates A,B by A8;
    then consider U,W be 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 thesis by A9,A10,A12;
  end;
  hence thesis by A1,Th32;
end;

theorem
  for T st T is T_4 & T is Lindelof & ex F be 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 such that
A1: T is T_4 and
A2: T is Lindelof;
  set CT=[#]T;
  given F be 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;
  per cases;
  suppose
    union F is empty;
    then CT={}T by A4,SETFAM_1:45;
    hence thesis by Th6;
  end;
  suppose
A7: union F is non empty;
    then reconsider CT as non empty set;
    consider f be sequence of 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
      set CTT=[:bool CT,bool CT:];
      defpred P[object,object] means
for n,A,B st$1=[n,[A,B]] holds(Cl A meets Cl B
implies $2=[A,B]) & (Cl A misses Cl B implies ex G,H be 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 such that
A10:  A misses B;
A11:  Cl A=A & Cl B=B by PRE_TOPC:22;
A12:  for x be object st x in [:NAT,CTT:]ex y be object st P[x,y]
      proof
        let x be object;
        assume x in [:NAT,CTT:];
        then consider n9,ab be object such that
A13:    n9 in NAT and
A14:    ab in CTT and
A15:    x=[n9,ab] by ZFMISC_1:def 2;
        consider A9,B9 be object such that
A16:    A9 in bool CT & B9 in bool CT and
A17:    ab=[A9,B9] by A14,ZFMISC_1:def 2;
        reconsider A9,B9 as Subset of T by A16;
        per cases;
        suppose
A18:      Cl A9 meets Cl B9;
          take ab;
          let n,A,B;
          assume x=[n,[A,B]];
          then
A19:      ab=[A,B] by A15,XTUPLE_0:1;
          then A=A9 by A17,XTUPLE_0:1;
          hence thesis by A17,A18,A19,XTUPLE_0:1;
        end;
        suppose
A20:      Cl A9 misses Cl B9;
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;
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 be 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;
            then consider x be object such that
A33:        x in af\/Cl A9 & x in bf\/Cl B9 by XBOOLE_0:3;
            per cases by A33,XBOOLE_0:def 3;
            suppose
              x in af & x in bf or x in Cl A9 & x in Cl B9;
              hence contradiction by A20,A28,XBOOLE_0:3;
            end;
            suppose
A34:          x in af & x in Cl B9;
              then x in Bf by A26,XBOOLE_0:def 4;
              hence contradiction by A28,A31,A34,XBOOLE_0:3;
            end;
            suppose
A35:          x in bf & x in Cl A9;
              then x in Af by A26,XBOOLE_0:def 4;
              hence contradiction by A28,A30,A35,XBOOLE_0:3;
            end;
          end;
          bf is closed & af is closed by A22,A26,TSEP_1:8;
          then consider U,W be 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];
          let n,A,B;
          assume
A39:      x=[n,[A,B]];
          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 thesis by A17,A20,A38,A41,A42,A43,A44,XTUPLE_0:1;
        end;
      end;
      consider GH be Function such that
      dom GH=[:NAT,CTT:] and
A45:  for x be object st x in [:NAT,CTT:] holds P[x,GH.x]
from CLASSES1:
      sch 1( A12);
      deffunc gh(set,set)=GH.[$1,$2];
      consider ghSeq be Function such that
A46:  dom ghSeq=NAT and
A47:  ghSeq.0=[A,B] and
A48:  for n holds ghSeq.(n+1)=gh(n,ghSeq.n) from NAT_1:sch 11;
      defpred R[Nat] means ghSeq.$1 in CTT & for A,B st A=(ghSeq.$1)`1 & B=(
      ghSeq.$1)`2 holds Cl A misses Cl B;
A49:  for n st R[n] holds R[n+1]
      proof
        let n such that
A50:    R[n];
        consider A,B be object 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,B as Subset of T by A51;
        n in NAT by ORDINAL1:def 12;
        then
A53:    [n,ghSeq.n] in [:NAT,CTT:] by A50,ZFMISC_1:87;
        Cl A misses Cl B by A50,A52;
        then consider G,H be 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;
        thus thesis by A55,A56;
      end;
A57:  R[0] by A10,A11,A47;
A58:  for n holds R[n] from NAT_1:sch 2(A57,A49);
      rng ghSeq c=CTT
      proof
        let y be object;
        assume y in rng ghSeq;
        then ex x be object st x in dom ghSeq & ghSeq.x=y by FUNCT_1:def 3;
        hence thesis by A46,A58;
      end;
      then reconsider ghSeq as sequence of CTT by A46,FUNCT_2:2;
      set g=pr1 ghSeq,h=pr2 ghSeq;
A59:  h.0=[A,B]`2 by A47,FUNCT_2:def 6
        .=B;
      reconsider RngH=rng(h^\1),RngG=rng(g^\1) as Subset-Family of T;
A60:  g.0=[A,B]`1 by A47,FUNCT_2:def 5
        .=A;
A61:  for n holds g.(n+1) in TOP & h.(n+1) in TOP & g.n c=g.(n+1) & h.n
      c=h .(n+1) & g.n misses h.n & f.n c=(g.(n+1))\/h.(n+1)
      proof
        let n;
        consider A,B be object such that
A62:    A in bool CT & B in bool CT and
A63:    ghSeq.n=[A,B] by ZFMISC_1:def 2;
        reconsider A,B as Subset of T by A62;
A64:    n in NAT by ORDINAL1:def 12;
        then
A65:    [n,ghSeq.n] in [:NAT,CTT:] by ZFMISC_1:87;
A66:    A=[A,B]`1;
        then
A67:    A=g.n by A46,A64,A63,MCART_1:def 12;
A68:    B=[A,B]`2;
        then
A69:    B=h.n by A46,A64,A63,MCART_1:def 13;
        Cl A misses Cl B by A58,A66,A68,A63;
        then consider G,H be 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
          .=g.(n+1) by A46,A74,MCART_1:def 12;
        hence g.(n+1) in TOP by PRE_TOPC:def 2;
A76:    H=[G,H]`2
          .=h.(n+1) by A46,A74,MCART_1:def 13;
        hence h.(n+1) in TOP by PRE_TOPC:def 2;
        A c=Cl A by PRE_TOPC:18;
        hence g.n c=g.(n+1) by A67,A71,A75;
        B c=Cl B by PRE_TOPC:18;
        hence h.n c=h.(n+1) by A69,A72,A76;
        A c=Cl A & B c=Cl B by PRE_TOPC:18;
        hence g.n misses h.n by A58,A66,A67,A68,A69,A63,XBOOLE_1:64;
        thus thesis by A70,A75,A76;
      end;
      then for n be Nat holds g.n c=g.(n+1);
      then
A77:  g is non-descending by KURATO_0:def 4;
A78:  RngH is open
      proof
A79:    RngH={h.n where n is Nat:n>=1} by SETLIM_1:6;
        let A be Subset of T;
        assume A in RngH;
        then consider n be Nat such that
A80:    h.n=A and
A81:    n>=1 by A79;
        reconsider n1=n-1 as Nat by A81,NAT_1:21;
        h.(n1+1) in TOP by A61;
        hence thesis by A80,PRE_TOPC:def 2;
      end;
      RngG is open
      proof
A82:    RngG={g.n where n is Nat:n>=1} by SETLIM_1:6;
        let A be Subset of T;
        assume A in RngG;
        then consider n be Nat such that
A83:    g.n=A and
A84:    n>=1 by A82;
        reconsider n1=n-1 as Nat by A84,NAT_1:21;
        g.(n1+1) in TOP by A61;
        hence thesis by A83,PRE_TOPC:def 2;
      end;
      then reconsider
      unionG=union RngG,unionH=union RngH as open Subset of T by A78,TOPS_2:19;
      for n be Nat holds h.n c=h.(n+1) by A61;
      then
A85:  h is non-descending by KURATO_0:def 4;
A86:  unionH misses unionG
      proof
        assume unionH meets unionG;
        then consider x be object such that
A87:    x in unionH and
A88:    x in unionG by XBOOLE_0:3;
        consider H be set such that
A89:    x in H and
A90:    H in RngH by A87,TARSKI:def 4;
        RngH={h.n where n is Nat:n>=1} by SETLIM_1:6;
        then consider i be Nat such that
A91:    h.i=H and
        i>=1 by A90;
        consider G be set such that
A92:    x in G and
A93:    G in RngG by A88,TARSKI:def 4;
        RngG={g.n where n is Nat:n>=1} by SETLIM_1:6;
        then consider j be Nat such that
A94:    g.j=G and
        j>=1 by A93;
        per cases;
        suppose
A95:      i<=j;
A96:      g.j misses h.j by A61;
          h.i c=h.j by A85,A95,PROB_1:def 5;
          hence contradiction by A92,A94,A89,A91,A96,XBOOLE_0:3;
        end;
        suppose
A97:      i>=j;
A98:      g.i misses h.i by A61;
          g.j c=g.i by A77,A97,PROB_1:def 5;
          hence contradiction by A92,A94,A89,A91,A98,XBOOLE_0:3;
        end;
      end;
A99:  CT c=unionH\/unionG
      proof
        let x be object;
        assume x in CT;
        then reconsider x as Point of T;
        union F=CT by A4,SETFAM_1:45;
        then consider X be set such that
A100:   x in X and
A101:   X in rng f by A8,TARSKI:def 4;
        consider n be object such that
A102:   n in dom f and
A103:   f.n=X by A101,FUNCT_1:def 3;
        reconsider n as Element of NAT by A102;
A104:   n+1>=1 by NAT_1:12;
A105:   f.n c=(g.(n+1))\/h.(n+1) by A61;
        per cases by A100,A103,A105,XBOOLE_0:def 3;
        suppose
A106:     x in g.(n+1);
          RngG={g.i where i is Nat:i>=1} by SETLIM_1:6;
          then g.(n+1) in RngG by A104;
          then x in unionG by A106,TARSKI:def 4;
          hence thesis by XBOOLE_0:def 3;
        end;
        suppose
A107:     x in h.(n+1);
          RngH={h.i where i is Nat:i>=1} by SETLIM_1:6;
          then h.(n+1) in RngH by A104;
          then x in unionH by A107,TARSKI:def 4;
          hence thesis by XBOOLE_0:def 3;
        end;
      end;
      then CT=unionH\/unionG;
      then unionH=unionG` & unionG=unionH` by A86,PRE_TOPC:5;
      then reconsider unionG,unionH as closed Subset of T;
      take unionG,unionH;
      thus unionG misses unionH by A86;
      thus unionG\/unionH=[#]T by A99;
      RngG={g.i where i is Nat:i>=1} by SETLIM_1:6;
      then g.1 in RngG;
      then
A108: g.1 c=unionG by ZFMISC_1:74;
      g.0 c=g.(0+1) by A61;
      hence A c=unionG by A108,A60;
      RngH={h.i where i is Nat:i>=1} by SETLIM_1:6;
      then h.1 in RngH;
      then
A109: h.1 c=unionH by ZFMISC_1:74;
      h.0 c=h.(0+1) by A61;
      hence B c=unionH by A109,A59;
    end;
    hence thesis by A1,Th32;
  end;
end;

reserve TM for metrizable TopSpace;

::  Teoria wymiaru Th 1.2.11

theorem Th37:
  for A,B be closed Subset of TM st A misses B for Null be
  finite-ind Subset of TM st ind Null<=0 & TM|Null is second-countable ex L be
  Subset of TM st L separates A,B & L misses Null
proof
  let A,B be closed Subset of TM;
  assume A misses B;
  then consider U,W be 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 such that
A3: ind Null<=0 & TM|Null is second-countable;
  set TN=TM|Null;
A4: [#]TN=Null by PRE_TOPC:def 5;
  then reconsider Un=Cl U/\Null,Wn=Cl W/\Null as Subset of TN 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 TN=ind Null by Lm5;
  Un is closed & Wn is closed by A4,TSP_1:def 2;
  then {}TN separates Un,Wn by A3,A5,A6,Th35;
  then consider L be Subset of TM such that
A7: L separates A,B and
A8: Null/\L c={}TN by A1,A2,METRIZTS:26;
  take L;
  Null/\L={} by A8;
  hence thesis by A7;
end;

::  Teoria wymiaru Th 1.2.12

theorem Th38:
  for Null be Subset of TM st TM|Null is second-countable holds
  Null is finite-ind & ind Null<=0 iff for p be Point of TM,U be open Subset of
  TM st p in U ex W be open Subset of TM st p in W & W c=U & Null misses Fr W
proof
  let Null be Subset of TM such that
A1: TM|Null is second-countable;
  hereby
    assume
A2: Null is finite-ind & ind Null<=0;
    let p be Point of TM,U be open Subset of TM such that
A3: p in U;
    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;
    TM is non empty by A3;
    then consider L be Subset of TM such that
A5: L separates P,U` and
A6: L misses Null by A1,A2,A4,Th37;
    consider W,W1 be 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 c=W1` & W1`c=U`` by A8,A9,SUBSET_1:12,23;
    hence p in W & W c=U by A7,ZFMISC_1:31;
    thus Null misses Fr W
    proof
      assume Null meets Fr W;
      then consider x be object 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,def 5;
      hence contradiction by A9,TSEP_1:36;
    end;
  end;
  set TN=TM|Null;
  assume
A15: for p be Point of TM,U be open Subset of TM st p in U ex W be open
  Subset of TM st p in W & W c=U & Null misses Fr W;
A16: for p be Point of TN,U be open Subset of TN st p in U ex W be open
  Subset of TN st p in W & W c=U & Fr W is finite-ind & ind Fr W<=0-1
  proof
    let p be Point of TN,U be open Subset of TN such that
A17: p in U;
A18: [#]TN=Null by PRE_TOPC:def 5;
    then p in Null by A17;
    then reconsider p9=p as Point of TM;
    consider U9 be Subset of TM such that
A19: U9 is open and
A20: U=U9/\the carrier of TN by TSP_1:def 1;
    p9 in U9 by A17,A20,XBOOLE_0:def 4;
    then consider W9 be 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 TN as Subset of TN by XBOOLE_1:17;
    reconsider W as open Subset of TN by TSP_1:def 1;
    take W;
    thus p in W & W c=U by A17,A20,A21,XBOOLE_0:def 4,XBOOLE_1:26;
A23: Fr W9/\Null={} by A22;
    Fr W c=Fr W9/\Null by A18,Th1;
    hence thesis by A23,Th6;
  end;
  then
A24: TN is finite-ind by Th15;
  then
A25: Null is finite-ind by Th18;
  ind TN<=0 by A16,A24,Th16;
  hence thesis by A25,Lm5;
end;

::  Teoria wymiaru Th 1.2.13

theorem Th39:
  for Null be Subset of TM st TM|Null is second-countable holds
Null is finite-ind & ind Null<=0 iff ex B be Basis of TM st for A be Subset of
  TM st A in B holds Null misses Fr A
proof
  set cTM=[#]TM;
  set TOP=the topology of TM;
  let Null be Subset of TM such that
A1: TM|Null is second-countable;
  hereby
    defpred P[object,object] means
for p be Point of TM,A be Subset of TM st$1=[p,A]
holds$2 in TOP & (not p in A implies $2={}TM) & (p in A implies ex W be 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;
A3: for x be object st x in [:cTM,TOP:]ex y be object st P[x,y]
    proof
      let x be object;
      assume x in [:cTM,TOP:];
      then consider p9,A9 be object such that
A4:   p9 in cTM and
A5:   A9 in TOP and
A6:   x=[p9,A9] by ZFMISC_1:def 2;
      reconsider p9 as Point of TM by A4;
      reconsider A9 as open Subset of TM by A5,PRE_TOPC:def 2;
      per cases;
      suppose
A7:     not p9 in A9;
        take{}TM;
        let p be Point of TM,A be Subset of TM such that
A8:     x=[p,A];
        p=p9 by A6,A8,XTUPLE_0:1;
        hence thesis by A6,A7,A8,PRE_TOPC:def 2,XTUPLE_0:1;
      end;
      suppose
        p9 in A9;
        then consider W be open Subset of TM such that
A9:     p9 in W & W c=A9 & Null misses Fr W by A1,A2,Th38;
        take W;
        let p be Point of TM,A be Subset of TM;
        assume x=[p,A];
        then p=p9 & A=A9 by A6,XTUPLE_0:1;
        hence thesis by A9,PRE_TOPC:def 2;
      end;
    end;
    consider f be Function such that
A10: dom f=[:cTM,TOP:] and
A11: for x be object st x in [:cTM,TOP:] holds P[x,f.x]
from CLASSES1:sch
    1( A3);
A12: rng f c=TOP
    proof
      let y be object;
      assume y in rng f;
      then consider x be object such that
A13:  x in dom f and
A14:  f.x=y by FUNCT_1:def 3;
      ex p,A be object st p in cTM & A in TOP & x=[p,A]
by A10,A13,ZFMISC_1:def 2;
      hence thesis by A10,A11,A13,A14;
    end;
    then reconsider RNG=rng f as Subset-Family of TM by XBOOLE_1:1;
    now
      let A be Subset of TM;
      assume A is open;
      then
A15:  A in TOP by PRE_TOPC:def 2;
      let p be Point of TM such that
A16:  p in A;
A17:  [p,A] in [:cTM,TOP:] by A15,A16,ZFMISC_1:87;
      then consider W be 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 as Subset of TM;
      take W;
      thus W in RNG & p in W & W c=A by A10,A17,A18,FUNCT_1:def 3;
    end;
    then reconsider RNG as Basis of TM by A12,YELLOW_9:32;
    take RNG;
    let B be Subset of TM;
    assume B in RNG;
    then consider x be object such that
A19: x in dom f and
A20: f.x=B by FUNCT_1:def 3;
    consider p,A be object such that
A21: p in cTM and
A22: A in TOP and
A23: x=[p,A] by A10,A19,ZFMISC_1:def 2;
    reconsider A as set by TARSKI:1;
    per cases;
    suppose
      p in A;
      then ex W be 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;
    end;
    suppose
      not p in A;
      then B={}TM by A10,A11,A19,A20,A21,A22,A23;
      then Fr B={}TM by TOPGEN_1:14;
      hence Null misses Fr B;
    end;
  end;
  given B be Basis of TM such that
A24: for A be Subset of TM st A in B holds Null misses Fr A;
  for p be Point of TM,U be open Subset of TM st p in U ex W be open
  Subset of TM st p in W & W c=U & Null misses Fr W
  proof
    let p be Point of TM,U be open Subset of TM;
    assume p in U;
    then consider a be Subset of TM such that
A25: a in B and
A26: p in a & a c=U by YELLOW_9:31;
    B c=TOP by TOPS_2:64;
    then reconsider a as open Subset of TM by A25,PRE_TOPC:def 2;
    take a;
    thus thesis by A24,A25,A26;
  end;
  hence thesis by A1,Th38;
end;

::  Teoria wymiaru Th 1.5.2

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