:: Maximal Kolmogorov Subspaces of a Topological Space as Stone
:: Retracts of the Ambient Space
::  by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994-2012 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 XBOOLE_0, PRE_TOPC, SUBSET_1, TEX_4, RCOMP_1, TARSKI, STRUCT_0,
      TOPS_1, ZFMISC_1, SETFAM_1, FUNCT_1, RELAT_1, NATTRA_1, ORDINAL2,
      BORSUK_1, TSP_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELAT_1, RELSET_1,
      FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TEX_2,
      TEX_3, TEX_4, TSP_1;
 constructors TOPS_1, BORSUK_1, TSEP_1, TEX_2, TEX_4, TSP_1, TEX_3;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TSP_1;
 requirements BOOLE, SUBSET;
 definitions SUBSET_1, STRUCT_0, RELAT_1;
 theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, PRE_TOPC, TOPS_1, BORSUK_1,
      TSEP_1, TOPS_3, TEX_2, TEX_3, TEX_4, TSP_1, RELAT_1, XBOOLE_0, XBOOLE_1,
      SUBSET_1, RELSET_1;
 schemes TEX_2, FUNCT_2;

begin

:: 1. Maximal T_{0} Subsets.

definition
  let X be non empty TopSpace;
  let A be Subset of X;
  redefine attr A is T_0 means
  :Def1:
  for a, b being Point of X st a in A & b
  in A holds a <> b implies MaxADSet(a) misses MaxADSet(b);
  compatibility
  proof
    thus A is T_0 implies for a, b being Point of X st a in A & b in A holds a
    <> b implies MaxADSet(a) misses MaxADSet(b)
    proof
      assume
A1:   A is T_0;
      let a, b be Point of X;
      assume that
A2:   a in A and
A3:   b in A;
      assume
A4:   a <> b;
      now
        per cases by A1,A2,A3,A4,TSP_1:def 8;
        suppose
          ex V being Subset of X st V is open & a in V & not b in V;
          then consider V being Subset of X such that
A5:       V is open and
A6:       a in V and
A7:       not b in V;
          now
            take V;
            thus V is open by A5;
            thus MaxADSet(a) c= V by A5,A6,TEX_4:24;
            b in [#]X \ V by A7,XBOOLE_0:def 5;
            then MaxADSet(b) c= V` by A5,TEX_4:23;
            hence V misses MaxADSet(b) by SUBSET_1:23;
          end;
          hence (ex V being Subset of X st V is open & MaxADSet(a) c= V & V
misses MaxADSet(b)) or ex W being Subset of X st W is open & W misses MaxADSet(
          a) & MaxADSet(b) c= W;
        end;
        suppose
          ex W being Subset of X st W is open & not a in W & b in W;
          then consider W being Subset of X such that
A8:       W is open and
A9:       not a in W and
A10:      b in W;
          now
            take W;
            thus W is open by A8;
            a in [#]X \ W by A9,XBOOLE_0:def 5;
            then MaxADSet(a) c= W` by A8,TEX_4:23;
            hence W misses MaxADSet(a) by SUBSET_1:23;
            thus MaxADSet(b) c= W by A8,A10,TEX_4:24;
          end;
          hence (ex V being Subset of X st V is open & MaxADSet(a) c= V & V
misses MaxADSet(b)) or ex W being Subset of X st W is open & W misses MaxADSet(
          a) & MaxADSet(b) c= W;
        end;
      end;
      hence thesis by TEX_4:53;
    end;
    assume
A11: for a, b being Point of X st a in A & b in A holds a <> b implies
    MaxADSet(a) misses MaxADSet(b);
    now
      let a, b be Point of X;
      assume that
A12:  a in A and
A13:  b in A;
      assume a <> b;
      then
A14:  MaxADSet(a) misses MaxADSet(b) by A11,A12,A13;
      now
        per cases by A14,TEX_4:53;
        suppose
          ex V being Subset of X st V is open & MaxADSet(a) c= V & V
          misses MaxADSet(b);
          then consider V being Subset of X such that
A15:      V is open and
A16:      MaxADSet(a) c= V and
A17:      V misses MaxADSet(b);
          now
            take V;
            thus V is open by A15;
            {a} c= MaxADSet(a) by TEX_4:18;
            then a in MaxADSet(a) by ZFMISC_1:31;
            hence a in V by A16;
            now
              {b} c= MaxADSet(b) by TEX_4:18;
              then
A18:          b in MaxADSet(b) by ZFMISC_1:31;
              assume b in V;
              hence contradiction by A17,A18,XBOOLE_0:3;
            end;
            hence not b in V;
          end;
          hence (ex V being Subset of X st V is open & a in V & not b in V) or
          ex W being Subset of X st W is open & not a in W & b in W;
        end;
        suppose
          ex W being Subset of X st W is open & W misses MaxADSet(a)
          & MaxADSet(b) c= W;
          then consider W being Subset of X such that
A19:      W is open and
A20:      W misses MaxADSet(a) and
A21:      MaxADSet(b) c= W;
          now
            take W;
            thus W is open by A19;
            now
              {a} c= MaxADSet(a) by TEX_4:18;
              then
A22:          a in MaxADSet(a) by ZFMISC_1:31;
              assume a in W;
              hence contradiction by A20,A22,XBOOLE_0:3;
            end;
            hence not a in W;
            {b} c= MaxADSet(b) by TEX_4:18;
            then b in MaxADSet(b) by ZFMISC_1:31;
            hence b in W by A21;
          end;
          hence (ex V being Subset of X st V is open & a in V & not b in V) or
          ex W being Subset of X st W is open & not a in W & b in W;
        end;
      end;
      hence
      (ex V being Subset of X st V is open & a in V & not b in V) or ex W
      being Subset of X st W is open & not a in W & b in W;
    end;
    hence thesis by TSP_1:def 8;
  end;
end;

definition
  let X be non empty TopSpace;
  let A be Subset of X;
  redefine attr A is T_0 means
  :Def2:
  for a being Point of X st a in A holds A /\ MaxADSet(a) = {a};
  compatibility
  proof
    thus A is T_0 implies for a being Point of X st a in A holds A /\ MaxADSet
    (a) = {a}
    proof
      assume
A1:   A is T_0;
      let a be Point of X;
      assume
A2:   a in A;
      assume
A3:   A /\ MaxADSet(a) <> {a};
      {a} c= MaxADSet(a) by TEX_4:18;
      then a in MaxADSet(a) by ZFMISC_1:31;
      then a in A /\ MaxADSet(a) by A2,XBOOLE_0:def 4;
      then consider b being set such that
A4:   b in A /\ MaxADSet(a) and
A5:   b <> a by A3,ZFMISC_1:35;
      reconsider b as Point of X by A4;
      b in A by A4,XBOOLE_0:def 4;
      then
A6:   MaxADSet(a) misses MaxADSet(b) by A1,A2,A5,Def1;
      b in MaxADSet(a) by A4,XBOOLE_0:def 4;
      hence contradiction by A6,TEX_4:21;
    end;
    assume
A7: for a being Point of X st a in A holds A /\ MaxADSet(a) = {a};
    now
      let a, b be Point of X;
      assume that
A8:   a in A and
A9:   b in A;
A10:  A /\ MaxADSet(a) = {a} by A7,A8;
A11:  A /\ MaxADSet(b) = {b} by A7,A9;
      assume
A12:  a <> b;
      assume MaxADSet(a) meets MaxADSet(b);
      then {a} = {b} by A10,A11,TEX_4:22;
      hence contradiction by A12,ZFMISC_1:3;
    end;
    hence thesis by Def1;
  end;
end;

definition
  let X be non empty TopSpace;
  let A be Subset of X;
  redefine attr A is T_0 means
  for a being Point of X st a in A ex D being
  Subset of X st D is maximal_anti-discrete & A /\ D = {a};
  compatibility
  proof
    thus A is T_0 implies for a being Point of X st a in A ex D being Subset
    of X st D is maximal_anti-discrete & A /\ D = {a}
    proof
      assume
A1:   A is T_0;
      let a be Point of X;
      assume
A2:   a in A;
      take D = MaxADSet(a);
      thus D is maximal_anti-discrete by TEX_4:20;
      thus thesis by A1,A2,Def2;
    end;
    assume
A3: for a being Point of X st a in A ex D being Subset of X st D is
    maximal_anti-discrete & A /\ D = {a};
    now
      let a be Point of X;
      assume a in A;
      then consider D being Subset of X such that
A4:   D is maximal_anti-discrete and
A5:   A /\ D = {a} by A3;
      a in A /\ D by A5,ZFMISC_1:31;
      then a in D by XBOOLE_0:def 4;
      hence A /\ MaxADSet(a) = {a} by A4,A5,TEX_4:27;
    end;
    hence thesis by Def2;
  end;
end;

definition
  let Y be TopStruct;
  let IT be Subset of Y;
  attr IT is maximal_T_0 means
  :Def4:
  IT is T_0 & for D being Subset of Y st D is T_0 & IT c= D holds IT = D;
end;

theorem
  for Y0, Y1 being TopStruct, D0 being Subset of Y0, D1 being Subset of
  Y1 st the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds D0 is
  maximal_T_0 implies D1 is maximal_T_0
proof
  let Y0, Y1 be TopStruct, D0 be Subset of Y0, D1 be Subset of Y1;
  assume
A1: the TopStruct of Y0 = the TopStruct of Y1;
  assume
A2: D0 = D1;
  assume
A3: D0 is maximal_T_0;
A4: now
    let D be Subset of Y1;
    reconsider E = D as Subset of Y0 by A1;
    assume D is T_0;
    then
A5: E is T_0 by A1,TSP_1:3;
    assume D1 c= D;
    hence D1 = D by A2,A3,A5,Def4;
  end;
  D0 is T_0 by A3,Def4;
  then D1 is T_0 by A1,A2,TSP_1:3;
  hence thesis by A4,Def4;
end;

definition
  let X be non empty TopSpace;
  let M be Subset of X;
  redefine attr M is maximal_T_0 means
  :Def5:
  M is T_0 & MaxADSet(M) = the carrier of X;
  compatibility
  proof
    thus M is maximal_T_0 implies M is T_0 & MaxADSet(M) = the carrier of X
    proof
      assume
A1:   M is maximal_T_0;
      hence
A2:   M is T_0 by Def4;
      the carrier of X c= MaxADSet(M)
      proof
        assume not the carrier of X c= MaxADSet(M);
        then consider x being set such that
A3:     x in the carrier of X and
A4:     not x in MaxADSet(M) by TARSKI:def 3;
        reconsider x as Point of X by A3;
        set A = M \/ {x};
        for a being Point of X st a in A holds A /\ MaxADSet(a) = {a}
        proof
          let a be Point of X;
          assume a in A;
          then
A5:       a in M or a in {x} by XBOOLE_0:def 3;
          now
            per cases by A5,TARSKI:def 1;
            suppose
A6:           a in M;
              {x} /\ MaxADSet(a) = {}
              proof
                assume {x} /\ MaxADSet(a) <> {};
                then {x} meets MaxADSet(a) by XBOOLE_0:def 7;
                then
A7:             x in MaxADSet(a) by ZFMISC_1:50;
                {a} c= M by A6,ZFMISC_1:31;
                then MaxADSet({a}) c= MaxADSet(M) by TEX_4:31;
                then MaxADSet(a) c= MaxADSet(M) by TEX_4:28;
                hence contradiction by A4,A7;
              end;
              then A /\ MaxADSet(a) = (M /\ MaxADSet(a)) \/ {} by XBOOLE_1:23
                .= M /\ MaxADSet(a);
              hence thesis by A2,A6,Def2;
            end;
            suppose
A8:           a = x;
              then
A9:           {x} c= MaxADSet(a) by TEX_4:18;
              M /\ MaxADSet(a) = {}
              proof
A10:            M c= MaxADSet(M) by TEX_4:32;
                assume M /\ MaxADSet(a) <> {};
                then MaxADSet(a) /\ MaxADSet(M) <> {} by A10,XBOOLE_1:3,26;
                then MaxADSet(a) meets MaxADSet(M) by XBOOLE_0:def 7;
                then
A11:            MaxADSet(a) c= MaxADSet(M) by TEX_4:30;
                x in MaxADSet(a) by A9,ZFMISC_1:31;
                hence contradiction by A4,A11;
              end;
              then A /\ MaxADSet(a) = {} \/ ({x} /\ MaxADSet(a)) by XBOOLE_1:23
                .= {x} /\ MaxADSet(a);
              hence thesis by A8,TEX_4:18,XBOOLE_1:28;
            end;
          end;
          hence thesis;
        end;
        then
A12:    A is T_0 by Def2;
A13:    M c= MaxADSet(M) by TEX_4:32;
A14:    {x} c= A by XBOOLE_1:7;
        M c= A by XBOOLE_1:7;
        then M = A by A1,A12,Def4;
        then x in M by A14,ZFMISC_1:31;
        hence contradiction by A4,A13;
      end;
      hence thesis by XBOOLE_0:def 10;
    end;
    assume
A15: M is T_0;
    assume
A16: MaxADSet(M) = the carrier of X;
    for D being Subset of X st D is T_0 & M c= D holds M = D
    proof
      let D be Subset of X;
      assume
A17:  D is T_0;
      assume
A18:  M c= D;
      D c= M
      proof
        assume not D c= M;
        then consider x being set such that
A19:    x in D and
A20:    not x in M by TARSKI:def 3;
A21:    x in the carrier of X by A19;
        reconsider x as Point of X by A19;
        x in union {MaxADSet(a) where a is Point of X : a in M} by A16,A21,
TEX_4:def 11;
        then consider C being set such that
A22:    x in C and
A23:    C in {MaxADSet(a) where a is Point of X : a in M} by TARSKI:def 4;
        consider a being Point of X such that
A24:    C = MaxADSet(a) and
A25:    a in M by A23;
        M /\ MaxADSet(x) c= D /\ MaxADSet(x) by A18,XBOOLE_1:26;
        then
A26:    M /\ MaxADSet(x) c= {x} by A17,A19,Def2;
        MaxADSet(a) = MaxADSet(x) by A22,A24,TEX_4:21;
        then M /\ MaxADSet(x) = {a} by A15,A25,Def2;
        hence contradiction by A20,A25,A26,ZFMISC_1:18;
      end;
      hence thesis by A18,XBOOLE_0:def 10;
    end;
    hence thesis by A15,Def4;
  end;
end;

reserve X for non empty TopSpace;

theorem Th2:
  for M being Subset of X holds M is maximal_T_0 implies M is dense
proof
  let M be Subset of X;
  assume
A1: M is maximal_T_0;
  then MaxADSet(M) = [#]X by Def5;
  then
A2: Cl MaxADSet(M) = MaxADSet(M) by PRE_TOPC:22;
  MaxADSet(M) = the carrier of X by A1,Def5;
  then Cl M = the carrier of X by A2,TEX_4:62;
  hence thesis by TOPS_3:def 2;
end;

theorem Th3:
  for A being Subset of X st A is open or A is closed holds A is
  maximal_T_0 implies A is not proper
proof
  let A be Subset of X;
  assume A is open or A is closed;
  then
A1: A = MaxADSet(A) by TEX_4:56,60;
  assume A is maximal_T_0;
  then A = the carrier of X by A1,Def5;
  hence thesis by SUBSET_1:def 6;
end;

theorem Th4:
  for A being empty Subset of X holds A is not maximal_T_0
proof
  consider a being set such that
A1: a in the carrier of X by XBOOLE_0:def 1;
  reconsider a as Point of X by A1;
  let A be empty Subset of X;
  now
    take C = {a};
    thus C is T_0 & A c= C & A <> C by TSP_1:12,XBOOLE_1:2;
  end;
  hence thesis by Def4;
end;

theorem Th5:
  for M being Subset of X st M is maximal_T_0 for A being Subset of
  X st A is closed holds A = MaxADSet(M /\ A)
proof
  let M be Subset of X;
  assume
A1: M is maximal_T_0;
  let A be Subset of X;
  assume
A2: A is closed;
  then MaxADSet(M /\ A) = MaxADSet(M) /\ MaxADSet(A) by TEX_4:64;
  then
A3: MaxADSet(M /\ A) = MaxADSet(M) /\ A by A2,TEX_4:60;
  A = (the carrier of X) /\ A by XBOOLE_1:28;
  hence thesis by A1,A3,Def5;
end;

theorem Th6:
  for M being Subset of X st M is maximal_T_0 for A being Subset of
  X st A is open holds A = MaxADSet(M /\ A)
proof
  let M be Subset of X;
  assume
A1: M is maximal_T_0;
  let A be Subset of X;
  assume
A2: A is open;
  then MaxADSet(M /\ A) = MaxADSet(M) /\ MaxADSet(A) by TEX_4:65;
  then
A3: MaxADSet(M /\ A) = MaxADSet(M) /\ A by A2,TEX_4:56;
  A = (the carrier of X) /\ A by XBOOLE_1:28;
  hence thesis by A1,A3,Def5;
end;

theorem
  for M being Subset of X st M is maximal_T_0 for A being Subset of X
  holds Cl A = MaxADSet(M /\ Cl A) by Th5;

theorem
  for M being Subset of X st M is maximal_T_0 for A being Subset of X
  holds Int A = MaxADSet(M /\ Int A) by Th6;

definition
  let X be non empty TopSpace;
  let M be Subset of X;
  redefine attr M is maximal_T_0 means
  :Def6:
  for x being Point of X ex a
  being Point of X st a in M & M /\ MaxADSet(x) = {a};
  compatibility
  proof
    thus M is maximal_T_0 implies for x being Point of X ex a being Point of X
    st a in M & M /\ MaxADSet(x) = {a}
    proof
      assume
A1:   M is maximal_T_0;
      then
A2:   M is T_0 by Def4;
      let x be Point of X;
      x in the carrier of X;
      then x in MaxADSet(M) by A1,Def5;
      then x in union {MaxADSet(a) where a is Point of X : a in M} by
TEX_4:def 11;
      then consider C being set such that
A3:   x in C and
A4:   C in {MaxADSet(a) where a is Point of X : a in M} by TARSKI:def 4;
      consider a being Point of X such that
A5:   C = MaxADSet(a) and
A6:   a in M by A4;
      MaxADSet(a) = MaxADSet(x) by A3,A5,TEX_4:21;
      then M /\ MaxADSet(x) = {a} by A2,A6,Def2;
      hence thesis by A6;
    end;
    assume
A7: for x being Point of X ex a being Point of X st a in M & M /\
    MaxADSet(x) = {a};
    now
      let x be set;
A8:   M c= MaxADSet(M) by TEX_4:32;
      assume x in the carrier of X;
      then reconsider y = x as Point of X;
      consider a being Point of X such that
A9:   a in M and
A10:  M /\ MaxADSet(y) = {a} by A7;
      {a} c= MaxADSet(y) by A10,XBOOLE_1:17;
      then a in MaxADSet(y) by ZFMISC_1:31;
      then MaxADSet(y) /\ MaxADSet(M) <> {} by A9,A8,XBOOLE_0:def 4;
      then MaxADSet(y) meets MaxADSet(M) by XBOOLE_0:def 7;
      then
A11:  MaxADSet(y) c= MaxADSet(M) by TEX_4:30;
      {y} c= MaxADSet(y) by TEX_4:18;
      then y in MaxADSet(y) by ZFMISC_1:31;
      hence x in MaxADSet(M) by A11;
    end;
    then the carrier of X c= MaxADSet(M) by TARSKI:def 3;
    then
A12: MaxADSet(M) = the carrier of X by XBOOLE_0:def 10;
    for b being Point of X st b in M holds M /\ MaxADSet(b) = {b}
    proof
      let b be Point of X;
A13:  ex a being Point of X st a in M & M /\ MaxADSet(b) = {a} by A7;
      {b} c= MaxADSet(b) by TEX_4:18;
      then
A14:  b in MaxADSet(b) by ZFMISC_1:31;
      assume b in M;
      then b in M /\ MaxADSet(b) by A14,XBOOLE_0:def 4;
      hence thesis by A13,TARSKI:def 1;
    end;
    then M is T_0 by Def2;
    hence thesis by A12,Def5;
  end;
end;

theorem Th9:
  for A being Subset of X holds A is T_0 implies ex M being Subset
  of X st A c= M & M is maximal_T_0
proof
  let A be Subset of X;
  set D = [#]X \ MaxADSet(A);
  set F = {MaxADSet(d) where d is Point of X : d in D};
  now
    let C be set;
    assume C in F;
    then ex a being Point of X st C = MaxADSet(a) & a in D;
    hence C in bool the carrier of X;
  end;
  then reconsider F as Subset-Family of X by TARSKI:def 3;
  assume
A1: A is T_0;
  defpred X[Subset of X,set] means $2 in D & $2 in $1;
A2: D = (MaxADSet(A))`;
  then
A3: MaxADSet(A) misses D by SUBSET_1:24;
  A c= MaxADSet(A) by TEX_4:32;
  then A misses D by A2,SUBSET_1:24;
  then
A4: A /\ D = {} by XBOOLE_0:def 7;
  reconsider F as Subset-Family of X;
A5: for S being Subset of X st S in F ex x being Point of X st X[S,x]
  proof
    let S be Subset of X;
    assume S in F;
    then consider d being Point of X such that
A6: S = MaxADSet(d) and
A7: d in D;
    take d;
    {d} c= MaxADSet(d) by TEX_4:18;
    hence thesis by A6,A7,ZFMISC_1:31;
  end;
  consider f being Function of F,the carrier of X such that
A8: for S being Subset of X st S in F holds X[S,f.S] from TEX_2:sch 1(
  A5);
  set M = A \/ (f.: F);
  now
    let x be set;
    assume x in f.: F;
    then ex S being set st S in F & S in F & x = f.S by FUNCT_2:64;
    hence x in D by A8;
  end;
  then f.: F c= D by TARSKI:def 3;
  then
A9: MaxADSet(A) misses (f.:F) by A3,XBOOLE_1:63;
  thus ex M being Subset of X st A c= M & M is maximal_T_0
  proof
    take M;
    thus
A10: A c= M by XBOOLE_1:7;
    for x being Point of X ex a being Point of X st a in M & M /\
    MaxADSet(x) = {a}
    proof
      let x be Point of X;
A11:  [#]X = MaxADSet(A) \/ D by XBOOLE_1:45;
      now
        per cases by A11,XBOOLE_0:def 3;
        suppose
A12:      x in MaxADSet(A);
          now
            {x} c= MaxADSet(A) by A12,ZFMISC_1:31;
            then MaxADSet({x}) c= MaxADSet(A) by TEX_4:34;
            then MaxADSet(x) c= MaxADSet(A) by TEX_4:28;
            then (f.: F) misses MaxADSet(x) by A9,XBOOLE_1:63;
            then (f.: F) /\ MaxADSet(x) = {} by XBOOLE_0:def 7;
            then
A13:        M /\ MaxADSet(x) = (A /\ MaxADSet(x)) \/ {} by XBOOLE_1:23;
            x in union {MaxADSet(a) where a is Point of X : a in A} by A12,
TEX_4:def 11;
            then consider C being set such that
A14:        x in C and
A15:        C in {MaxADSet(a) where a is Point of X : a in A} by TARSKI:def 4;
            consider a being Point of X such that
A16:        C = MaxADSet(a) and
A17:        a in A by A15;
            take a;
            thus a in M by A10,A17;
            MaxADSet(a) = MaxADSet(x) by A14,A16,TEX_4:21;
            hence M /\ MaxADSet(x) = {a} by A1,A17,A13,Def2;
          end;
          hence thesis;
        end;
        suppose
A18:      x in D;
          then
A19:      MaxADSet(x) in F;
          now
            reconsider a = f.(MaxADSet(x)) as Point of X by A19,FUNCT_2:5;
            take a;
A20:        f.: F c= M by XBOOLE_1:7;
            now
              let y be set;
              assume
A21:          y in M /\ MaxADSet(x);
              then reconsider z = y as Point of X;
A22:          z in M by A21,XBOOLE_0:def 4;
A23:          z in MaxADSet(x) by A21,XBOOLE_0:def 4;
              then
A24:          MaxADSet(z) = MaxADSet(x) by TEX_4:21;
              now
                assume not MaxADSet(x) c= D;
                then MaxADSet(x) meets MaxADSet(A) by A2,SUBSET_1:23;
                then
A25:            MaxADSet(x) c= MaxADSet(A) by TEX_4:30;
                {x} c= MaxADSet(x) by TEX_4:18;
                then x in MaxADSet(x) by ZFMISC_1:31;
                hence contradiction by A3,A18,A25,XBOOLE_0:3;
              end;
              then not z in A by A4,A23,XBOOLE_0:def 4;
              then z in f.: F by A22,XBOOLE_0:def 3;
              then consider C being set such that
A26:          C in F and
              C in F and
A27:          z = f.C by FUNCT_2:64;
              reconsider C as Subset of X by A26;
              consider w being Point of X such that
A28:          C = MaxADSet(w) and
              w in D by A26;
              z in MaxADSet(w) by A8,A26,A27,A28;
              then f.(MaxADSet(w)) = a by A24,TEX_4:21;
              hence y in {a} by A27,A28,TARSKI:def 1;
            end;
            then
A29:        M /\ MaxADSet(x) c= {a} by TARSKI:def 3;
A30:        a in f.: F by A19,FUNCT_2:35;
            hence a in M by A20;
            a in MaxADSet(x) by A8,A19;
            then
A31:        {a} c= MaxADSet(x) by ZFMISC_1:31;
            {a} c= M by A20,A30,ZFMISC_1:31;
            then {a} c= M /\ MaxADSet(x) by A31,XBOOLE_1:19;
            hence M /\ MaxADSet(x) = {a} by A29,XBOOLE_0:def 10;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    hence M is maximal_T_0 by Def6;
  end;
end;

theorem Th10:
  ex M being Subset of X st M is maximal_T_0
proof
  set A = {}X;
  A is discrete by TEX_2:29;
  then consider M being Subset of X such that
  A c= M and
A1: M is maximal_T_0 by Th9,TSP_1:9;
  take M;
  thus thesis by A1;
end;

begin

:: 2. Maximal Kolmogorov Subspaces.

definition
  let Y be non empty TopStruct;
  let IT be SubSpace of Y;
  attr IT is maximal_T_0 means
  :Def7:
  for A being Subset of Y st A = the carrier of IT holds A is maximal_T_0;
end;

theorem Th11:
  for Y being non empty TopStruct, Y0 being SubSpace of Y, A being
  Subset of Y st A = the carrier of Y0 holds A is maximal_T_0 iff Y0 is
  maximal_T_0
proof
  let Y be non empty TopStruct, Y0 be SubSpace of Y, A be Subset of Y;
  assume
A1: A = the carrier of Y0;
  hereby
    assume A is maximal_T_0;
    then for A be Subset of Y st A = the carrier of Y0 holds A is maximal_T_0
    by A1;
    hence Y0 is maximal_T_0 by Def7;
  end;
  thus thesis by A1,Def7;
end;

Lm1: now
  let Z be non empty TopStruct;
  let Z0 be SubSpace of Z;
  [#]Z0 c= [#]Z by PRE_TOPC:def 4;
  hence the carrier of Z0 is Subset of Z;
end;

registration
  let Y be non empty TopStruct;
  cluster maximal_T_0 -> T_0 for non empty SubSpace of Y;
  coherence
  proof
    let Y0 be non empty SubSpace of Y;
    reconsider A = the carrier of Y0 as Subset of Y by Lm1;
    assume Y0 is maximal_T_0;
    then A is maximal_T_0 by Th11;
    then A is T_0 by Def4;
    hence thesis by TSP_1:13;
  end;
  cluster non T_0 -> non maximal_T_0 for non empty SubSpace of Y;
  coherence;
end;

definition
  let X be non empty TopSpace;
  let X0 be non empty SubSpace of X;
  redefine attr X0 is maximal_T_0 means
  X0 is T_0 & for Y0 being T_0 non empty
SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct
  of Y0;
  compatibility
  proof
    reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
    thus X0 is maximal_T_0 implies X0 is T_0 & for Y0 being T_0 non empty
SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct
    of Y0
    proof
      assume X0 is maximal_T_0;
      then
A1:   A is maximal_T_0 by Th11;
      then A is T_0 by Def4;
      hence X0 is T_0 by TSP_1:13;
      thus for Y0 being T_0 non empty SubSpace of X st X0 is SubSpace of Y0
      holds the TopStruct of X0 = the TopStruct of Y0
      proof
        let Y0 be T_0 non empty SubSpace of X;
        reconsider D = the carrier of Y0 as Subset of X by TSEP_1:1;
        assume X0 is SubSpace of Y0;
        then
A2:     A c= D by TSEP_1:4;
        D is T_0 by TSP_1:13;
        then A = D by A1,A2,Def4;
        hence thesis by TSEP_1:5;
      end;
    end;
    assume X0 is T_0;
    then
A3: A is T_0 by TSP_1:13;
    assume
A4: for Y0 being T_0 non empty SubSpace of X st X0 is SubSpace of Y0
    holds the TopStruct of X0 = the TopStruct of Y0;
    now
      let D be Subset of X;
      assume
A5:   D is T_0;
      assume
A6:   A c= D;
      then D <> {};
      then consider Y0 being T_0 strict non empty SubSpace of X such that
A7:   D = the carrier of Y0 by A5,TSP_1:18;
      X0 is SubSpace of Y0 by A6,A7,TSEP_1:4;
      hence A = D by A4,A7;
    end;
    then A is maximal_T_0 by A3,Def4;
    hence thesis by Th11;
  end;
end;

reserve X for non empty TopSpace;

theorem Th12:
  for A0 being non empty Subset of X st A0 is maximal_T_0 ex X0
being strict non empty SubSpace of X st X0 is maximal_T_0 & A0 = the carrier of
  X0
proof
  let A0 be non empty Subset of X;
  assume
A1: A0 is maximal_T_0;
  consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
  take X0;
  thus thesis by A1,A2,Th11;
end;

registration
  let X be non empty TopSpace;
  cluster maximal_T_0 -> dense for SubSpace of X;
  coherence
  proof
    let X0 be SubSpace of X;
    reconsider A = the carrier of X0 as Subset of X by Lm1;
    assume X0 is maximal_T_0;
    then A is maximal_T_0 by Th11;
    then A is dense by Th2;
    hence thesis by TEX_3:9;
  end;
  cluster non dense -> non maximal_T_0 for SubSpace of X;
  coherence;
  cluster open maximal_T_0 -> non proper for SubSpace of X;
  coherence
  proof
    let X0 be SubSpace of X;
    reconsider A = the carrier of X0 as Subset of X by Lm1;
    assume X0 is open;
    then
A1: A is open by TSEP_1:16;
    assume X0 is maximal_T_0;
    then A is maximal_T_0 by Th11;
    then A is non proper by A1,Th3;
    hence thesis by TEX_2:8;
  end;
  cluster open proper -> non maximal_T_0 for SubSpace of X;
  coherence;
  cluster proper maximal_T_0 -> non open for SubSpace of X;
  coherence;
  cluster closed maximal_T_0 -> non proper for SubSpace of X;
  coherence
  proof
    let X0 be SubSpace of X;
    reconsider A = the carrier of X0 as Subset of X by Lm1;
    assume X0 is closed;
    then
A2: A is closed by TSEP_1:11;
    assume X0 is maximal_T_0;
    then A is maximal_T_0 by Th11;
    then A is non proper by A2,Th3;
    hence thesis by TEX_2:8;
  end;
  cluster closed proper -> non maximal_T_0 for SubSpace of X;
  coherence;
  cluster proper maximal_T_0 -> non closed for SubSpace of X;
  coherence;
end;

theorem
  for Y0 being T_0 non empty SubSpace of X ex X0 being strict SubSpace
  of X st Y0 is SubSpace of X0 & X0 is maximal_T_0
proof
  let Y0 be T_0 non empty SubSpace of X;
  reconsider A = the carrier of Y0 as Subset of X by Lm1;
  A is T_0 by TSP_1:13;
  then consider M being Subset of X such that
A1: A c= M and
A2: M is maximal_T_0 by Th9;
  M is non empty by A2,Th4;
  then consider X0 being strict non empty SubSpace of X such that
A3: X0 is maximal_T_0 and
A4: M = the carrier of X0 by A2,Th12;
  take X0;
  thus thesis by A1,A3,A4,TSEP_1:4;
end;

registration
  let X be non empty TopSpace;
  cluster maximal_T_0 strict non empty for SubSpace of X;
  existence
  proof
    consider M being Subset of X such that
A1: M is maximal_T_0 by Th10;
    M is non empty by A1,Th4;
    then consider X0 being strict non empty SubSpace of X such that
A2: X0 is maximal_T_0 and
    M = the carrier of X0 by A1,Th12;
    take X0;
    thus thesis by A2;
  end;
end;

definition
  let X be non empty TopSpace;
  mode maximal_Kolmogorov_subspace of X is maximal_T_0 SubSpace of X;
end;

theorem Th14:
  for X0 being maximal_Kolmogorov_subspace of X for G being Subset
of X, G0 being Subset of X0 st G0 = G holds G0 is open iff MaxADSet(G) is open
  & G0 = MaxADSet(G) /\ the carrier of X0
proof
  let X0 be maximal_Kolmogorov_subspace of X;
  let G be Subset of X, G0 be Subset of X0;
  reconsider M = the carrier of X0 as Subset of X by Lm1;
  assume
A1: G0 = G;
A2: M is maximal_T_0 by Th11;
  thus G0 is open implies MaxADSet(G) is open & G0 = MaxADSet(G) /\ the
  carrier of X0
  proof
    assume G0 is open;
    then
A3: ex H being Subset of X st H is open & G0 = H /\ M by TSP_1:def 1;
    hence MaxADSet(G) is open by A2,A1,Th6;
    thus thesis by A2,A1,A3,Th6;
  end;
  assume
A4: MaxADSet(G) is open;
  assume G0 = MaxADSet(G) /\ the carrier of X0;
  hence thesis by A4,TSP_1:def 1;
end;

theorem
  for X0 being maximal_Kolmogorov_subspace of X for G being Subset of X
holds G is open iff G = MaxADSet(G) & ex G0 being Subset of X0 st G0 is open &
  G0 = G /\ the carrier of X0
proof
  let X0 be maximal_Kolmogorov_subspace of X;
  let G be Subset of X;
  reconsider M = the carrier of X0 as Subset of X by Lm1;
  thus G is open implies G = MaxADSet(G) & ex G0 being Subset of X0 st G0 is
  open & G0 = G /\ the carrier of X0
  proof
    reconsider G0 = G /\ M as Subset of X0 by XBOOLE_1:17;
    reconsider G0 as Subset of X0;
    assume
A1: G is open;
    hence G = MaxADSet(G) by TEX_4:56;
    take G0;
    thus G0 is open by A1,TSP_1:def 1;
    thus thesis;
  end;
  assume
A2: G = MaxADSet(G);
  given G0 being Subset of X0 such that
A3: G0 is open and
A4: G0 = G /\ the carrier of X0;
  set E = G0;
  E c= M;
  then reconsider E as Subset of X by XBOOLE_1:1;
A5: E c= MaxADSet(G) by A2,A4,XBOOLE_1:17;
A6: M is maximal_T_0 by Th11;
  for x being set st x in G holds x in MaxADSet(E)
  proof
    let x be set;
    assume
A7: x in G;
    then reconsider a = x as Point of X;
    consider b being Point of X such that
A8: b in M and
A9: M /\ MaxADSet(a) = {b} by A6,Def6;
A10: {b} c= MaxADSet(a) by A9,XBOOLE_1:17;
    {a} c= G by A7,ZFMISC_1:31;
    then MaxADSet({a}) c= G by A2,TEX_4:34;
    then MaxADSet(a) c= G by TEX_4:28;
    then {b} c= G by A10,XBOOLE_1:1;
    then b in G by ZFMISC_1:31;
    then b in E by A4,A8,XBOOLE_0:def 4;
    then {b} c= E by ZFMISC_1:31;
    then MaxADSet({b}) c= MaxADSet(E) by TEX_4:31;
    then
A11: MaxADSet(b) c= MaxADSet(E) by TEX_4:28;
    b in MaxADSet(a) by A10,ZFMISC_1:31;
    then MaxADSet(b) = MaxADSet(a) by TEX_4:21;
    then {a} c= MaxADSet(b) by TEX_4:18;
    then a in MaxADSet(b) by ZFMISC_1:31;
    hence thesis by A11;
  end;
  then
A12: G c= MaxADSet(E) by TARSKI:def 3;
  MaxADSet(E) is open by A3,Th14;
  hence thesis by A2,A5,A12,TEX_4:35;
end;

theorem Th16:
  for X0 being maximal_Kolmogorov_subspace of X for F being Subset
  of X, F0 being Subset of X0 st F0 = F holds F0 is closed iff MaxADSet(F) is
  closed & F0 = MaxADSet(F) /\ the carrier of X0
proof
  let X0 be maximal_Kolmogorov_subspace of X;
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  let F be Subset of X, F0 be Subset of X0;
  assume
A1: F0 = F;
A2: M is maximal_T_0 by Th11;
  thus F0 is closed implies MaxADSet(F) is closed & F0 = MaxADSet(F) /\ the
  carrier of X0
  proof
    assume F0 is closed;
    then
A3: ex H being Subset of X st H is closed & F0 = H /\ M by TSP_1:def 2;
    hence MaxADSet(F) is closed by A2,A1,Th5;
    thus thesis by A2,A1,A3,Th5;
  end;
  assume
A4: MaxADSet(F) is closed;
  assume F0 = MaxADSet(F) /\ the carrier of X0;
  hence thesis by A4,TSP_1:def 2;
end;

theorem
  for X0 being maximal_Kolmogorov_subspace of X for F being Subset of X
  holds F is closed iff F = MaxADSet(F) & ex F0 being Subset of X0 st F0 is
  closed & F0 = F /\ the carrier of X0
proof
  let X0 be maximal_Kolmogorov_subspace of X;
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  let F be Subset of X;
  thus F is closed implies F = MaxADSet(F) & ex F0 being Subset of X0 st F0 is
  closed & F0 = F /\ the carrier of X0
  proof
    set F0 = F /\ M;
    reconsider F0 as Subset of X0 by XBOOLE_1:17;
    assume
A1: F is closed;
    hence F = MaxADSet(F) by TEX_4:60;
    take F0;
    thus F0 is closed by A1,TSP_1:def 2;
    thus thesis;
  end;
  assume
A2: F = MaxADSet(F);
  given F0 being Subset of X0 such that
A3: F0 is closed and
A4: F0 = F /\ the carrier of X0;
  set E = F0;
  E c= M;
  then reconsider E as Subset of X by XBOOLE_1:1;
A5: E c= MaxADSet(F) by A2,A4,XBOOLE_1:17;
A6: M is maximal_T_0 by Th11;
  for x being set st x in F holds x in MaxADSet(E)
  proof
    let x be set;
    assume
A7: x in F;
    then reconsider a = x as Point of X;
    consider b being Point of X such that
A8: b in M and
A9: M /\ MaxADSet(a) = {b} by A6,Def6;
A10: {b} c= MaxADSet(a) by A9,XBOOLE_1:17;
    {a} c= F by A7,ZFMISC_1:31;
    then MaxADSet({a}) c= F by A2,TEX_4:34;
    then MaxADSet(a) c= F by TEX_4:28;
    then {b} c= F by A10,XBOOLE_1:1;
    then b in F by ZFMISC_1:31;
    then b in E by A4,A8,XBOOLE_0:def 4;
    then {b} c= E by ZFMISC_1:31;
    then MaxADSet({b}) c= MaxADSet(E) by TEX_4:31;
    then
A11: MaxADSet(b) c= MaxADSet(E) by TEX_4:28;
    b in MaxADSet(a) by A10,ZFMISC_1:31;
    then MaxADSet(b) = MaxADSet(a) by TEX_4:21;
    then {a} c= MaxADSet(b) by TEX_4:18;
    then a in MaxADSet(b) by ZFMISC_1:31;
    hence thesis by A11;
  end;
  then
A12: F c= MaxADSet(E) by TARSKI:def 3;
  MaxADSet(E) is closed by A3,Th16;
  hence thesis by A2,A5,A12,TEX_4:35;
end;

begin

:: 3. Stone Retraction Mapping Theorems.

reserve X for non empty TopSpace,
  X0 for non empty maximal_Kolmogorov_subspace of X;

theorem Th18:
  for r being Function of X,X0 for M being Subset of X st M = the
  carrier of X0 holds (for a being Point of X holds M /\ MaxADSet(a) = {r.a})
  implies r is continuous Function of X,X0
proof
  let r be Function of X,X0;
  let M be Subset of X;
  assume
A1: M = the carrier of X0;
  reconsider N = M as Subset of X;
  assume
A2: for a being Point of X holds M /\ MaxADSet(a) = {r.a};
A3: N is maximal_T_0 by A1,Th11;
  then
A4: N is T_0 by Def4;
  for F being Subset of X0 holds F is closed implies r" F is closed
  proof
    let F be Subset of X0;
    reconsider E = F as Subset of X by A1,XBOOLE_1:1;
    set R = {MaxADSet(a) where a is Point of X : a in E};
    now
      let x be set;
      assume
A5:   x in r" F;
      then reconsider b = x as Point of X;
A6:   r.b in F by A5,FUNCT_2:38;
      E c= the carrier of X;
      then reconsider a = r.b as Point of X by A6;
      MaxADSet(a) in R by A6;
      then
A7:   MaxADSet(a) c= union R by ZFMISC_1:74;
      M /\ MaxADSet(b) = {a} by A2;
      then a in M /\ MaxADSet(b) by ZFMISC_1:31;
      then a in MaxADSet(b) by XBOOLE_0:def 4;
      then
A8:   MaxADSet(a) = MaxADSet(b) by TEX_4:21;
A9:   {b} c= MaxADSet(b) by TEX_4:18;
      b in {b} by TARSKI:def 1;
      then b in MaxADSet(a) by A8,A9;
      hence x in union R by A7;
    end;
    then
A10: r" F c= union R by TARSKI:def 3;
    assume F is closed;
    then ex P being Subset of X st P is closed & P /\ [#]X0 = F by PRE_TOPC:13;
    then
A11: MaxADSet(E) is closed by A1,A3,Th5;
    now
      let C be set;
      assume C in R;
      then consider a being Point of X such that
A12:  C = MaxADSet(a) and
A13:  a in E;
      now
        let x be set;
        assume
A14:    x in C;
        then reconsider b = x as Point of X by A12;
A15:    M /\ MaxADSet(b) = {r.b} by A2;
A16:    M /\ MaxADSet(a) = {a} by A1,A4,A13,Def2;
        MaxADSet(a) = MaxADSet(b) by A12,A14,TEX_4:21;
        then a = r.x by A16,A15,ZFMISC_1:3;
        hence x in r" F by A12,A13,A14,FUNCT_2:38;
      end;
      hence C c= r" F by TARSKI:def 3;
    end;
    then
A17: union R c= r" F by ZFMISC_1:76;
    union R = MaxADSet(E) by TEX_4:def 11;
    hence thesis by A11,A17,A10,XBOOLE_0:def 10;
  end;
  hence thesis by PRE_TOPC:def 6;
end;

theorem
  for r being Function of X,X0 holds (for a being Point of X holds r.a
  in MaxADSet(a)) implies r is continuous Function of X,X0
proof
  let r be Function of X,X0;
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  assume
A1: for a being Point of X holds r.a in MaxADSet(a);
  M is maximal_T_0 by Th11;
  then
A2: M is T_0 by Def4;
A3: M c= the carrier of X;
  for a being Point of X holds M /\ MaxADSet(a) = {r.a}
  proof
    let a be Point of X;
    reconsider s = r.a as Point of X by A3,TARSKI:def 3;
A4: s in MaxADSet(a) by A1;
    M /\ MaxADSet(s) = {s} by A2,Def2;
    hence thesis by A4,TEX_4:21;
  end;
  hence thesis by Th18;
end;

theorem Th20:
  for r being continuous Function of X,X0 for M being Subset of X
st M = the carrier of X0 holds (for a being Point of X holds M /\ MaxADSet(a) =
  {r.a}) implies r is being_a_retraction
proof
  let r be continuous Function of X,X0;
  let M be Subset of X;
  reconsider N = M as Subset of X;
  assume
A1: M = the carrier of X0;
  then N is maximal_T_0 by Th11;
  then
A2: N is T_0 by Def4;
  assume
A3: for a being Point of X holds M /\ MaxADSet(a) = {r.a};
  for x being Point of X st x in the carrier of X0 holds r.x = x
  proof
    let x be Point of X;
    assume x in the carrier of X0;
    then
A4: M /\ MaxADSet(x) = {x} by A1,A2,Def2;
    M /\ MaxADSet(x) = {r.x} by A3;
    hence thesis by A4,ZFMISC_1:3;
  end;
  hence thesis by BORSUK_1:def 16;
end;

theorem Th21:
  for r being continuous Function of X,X0 holds (for a being Point
  of X holds r.a in MaxADSet(a)) implies r is being_a_retraction
proof
  let r be continuous Function of X,X0;
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  assume
A1: for a being Point of X holds r.a in MaxADSet(a);
  M is maximal_T_0 by Th11;
  then
A2: M is T_0 by Def4;
A3: M c= the carrier of X;
  for a being Point of X holds M /\ MaxADSet(a) = {r.a}
  proof
    let a be Point of X;
    reconsider s = r.a as Point of X by A3,TARSKI:def 3;
A4: s in MaxADSet(a) by A1;
    M /\ MaxADSet(s) = {s} by A2,Def2;
    hence thesis by A4,TEX_4:21;
  end;
  hence thesis by Th20;
end;

theorem Th22:
  ex r being continuous Function of X,X0 st r is being_a_retraction
proof
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  defpred X[Point of X,set] means M /\ MaxADSet $1 = {$2};
A1: M is maximal_T_0 by Th11;
A2: for x being Point of X ex a being Point of X0 st X[x,a]
  proof
    let x be Point of X;
    consider a being Point of X such that
A3: a in M and
A4: M /\ MaxADSet(x) = {a} by A1,Def6;
    reconsider a as Point of X0 by A3;
    take a;
    thus thesis by A4;
  end;
  consider r being Function of X,X0 such that
A5: for x being Point of X holds X[x,r.x] from FUNCT_2:sch 3(A2);
  reconsider r as continuous Function of X,X0 by A5,Th18;
  take r;
  thus thesis by A5,Th20;
end;

theorem
  X0 is_a_retract_of X
proof
  ex r being continuous Function of X,X0 st r is being_a_retraction by Th22;
  hence thesis by BORSUK_1:def 17;
end;

Lm2: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for a being Point of X, b being Point of X0 st a = b holds r" Cl {b} =
Cl {a}
proof
  let r be continuous Function of X,X0;
  assume
A1: r is being_a_retraction;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  let a be Point of X, b be Point of X0;
A2: b in {b} by TARSKI:def 1;
  assume
A3: a = b;
  then r.a = b by A1,BORSUK_1:def 16;
  then
A4: a in r" {b} by A2,FUNCT_2:38;
A5: A is maximal_T_0 by Th11;
A6: r" Cl {b} c= Cl {a}
  proof
    assume not r" Cl {b} c= Cl {a};
    then consider c being set such that
A7: c in r" Cl {b} and
A8: not c in Cl {a} by TARSKI:def 3;
    reconsider c as Point of X by A7;
    consider d being Point of X such that
A9: d in A and
A10: A /\ MaxADSet(c) = {d} by A5,Def6;
A11: {d} c= MaxADSet(c) by A10,XBOOLE_1:17;
    r" Cl {b} is closed by PRE_TOPC:def 6;
    then MaxADSet(c) c= r" Cl {b} by A7,TEX_4:23;
    then {d} c= r" Cl {b} by A11,XBOOLE_1:1;
    then
A12: d in r" Cl {b} by ZFMISC_1:31;
    reconsider e = d as Point of X0 by A9;
    {c} c= MaxADSet(c) by TEX_4:18;
    then
A13: c in MaxADSet(c) by ZFMISC_1:31;
A14: Cl {b} c= Cl {a} by A3,TOPS_3:53;
    r.d = e by A1,BORSUK_1:def 16;
    then e in Cl {b} by A12,FUNCT_2:38;
    then
A15: MaxADSet(d) c= Cl {a} by A14,TEX_4:23;
    d in MaxADSet(c) by A11,ZFMISC_1:31;
    then MaxADSet(d) = MaxADSet(c) by TEX_4:21;
    hence contradiction by A8,A13,A15;
  end;
A16: r" Cl {b} is closed by PRE_TOPC:def 6;
  r" {b} c= r" Cl {b} by PRE_TOPC:18,RELAT_1:143;
  then {a} c= r" Cl {b} by A4,ZFMISC_1:31;
  then Cl {a} c= r" Cl {b} by A16,TOPS_1:5;
  hence thesis by A6,XBOOLE_0:def 10;
end;

Lm3: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for A being Subset of X st A = the carrier of X0 for a being Point of X
holds A /\ MaxADSet(a) = {r.a}
proof
  let r be continuous Function of X,X0;
  assume
A1: r is being_a_retraction;
  let A be Subset of X;
  reconsider N = A as Subset of X;
  assume
A2: A = the carrier of X0;
  let a be Point of X;
A3: N is maximal_T_0 by A2,Th11;
  then consider c being Point of X such that
A4: c in A and
A5: A /\ MaxADSet(a) = {c} by Def6;
A6: {c} c= MaxADSet(c) by TEX_4:18;
  r.a in A by A2;
  then reconsider d = r.a as Point of X;
  {r.a} c= Cl {r.a} by PRE_TOPC:18;
  then
A7: r.a in Cl {r.a} by ZFMISC_1:31;
  {c} c= MaxADSet(a) by A5,XBOOLE_1:17;
  then c in MaxADSet(a) by ZFMISC_1:31;
  then
A8: MaxADSet(c) = MaxADSet(a) by TEX_4:21;
  reconsider b = c as Point of X0 by A2,A4;
A9: {a} c= MaxADSet(a) by TEX_4:18;
A10: r" Cl {b} = Cl {c} by A1,Lm2;
  then {c} c= r" Cl {b} by PRE_TOPC:18;
  then c in r" Cl {b} by ZFMISC_1:31;
  then MaxADSet(a) c= r" Cl {b} by A10,A8,TEX_4:23;
  then {a} c= r" Cl {b} by A9,XBOOLE_1:1;
  then a in r" Cl {b} by ZFMISC_1:31;
  then
A11: r.a in Cl {b} by FUNCT_2:38;
  r" Cl {r.a} = Cl {d} by A1,Lm2;
  then a in Cl {d} by A7,FUNCT_2:38;
  then MaxADSet(c) c= Cl {d} by A8,TEX_4:23;
  then {c} c= Cl {d} by A6,XBOOLE_1:1;
  then
A12: Cl {c} c= Cl {d} by TOPS_1:5;
  Cl {b} c= Cl {c} by TOPS_3:53;
  then {d} c= Cl {c} by A11,ZFMISC_1:31;
  then Cl {d} c= Cl {c} by TOPS_1:5;
  then Cl {d} = Cl {c} by A12,XBOOLE_0:def 10;
  then
A13: MaxADSet(d) = MaxADSet(a) by A8,TEX_4:49;
  N is T_0 by A3,Def4;
  hence thesis by A2,A13,Def2;
end;

Lm4: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for a being Point of X, b being Point of X0 st a = b holds MaxADSet(a)
c= r" {b}
proof
  let r be continuous Function of X,X0;
  assume
A1: r is being_a_retraction;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  let a be Point of X, b be Point of X0;
  assume
A2: a = b;
  assume not MaxADSet(a) c= r" {b};
  then consider s being set such that
A3: s in MaxADSet(a) and
A4: not s in r" {b} by TARSKI:def 3;
  reconsider s as Point of X by A3;
A5: MaxADSet(a) = MaxADSet(s) by A3,TEX_4:21;
A6: {s} c= MaxADSet(s) by TEX_4:18;
A7: r" Cl {b} = Cl {a} by A1,A2,Lm2;
  then {a} c= r" Cl {b} by PRE_TOPC:18;
  then a in r" Cl {b} by ZFMISC_1:31;
  then MaxADSet(s) c= r" Cl {b} by A7,A5,TEX_4:23;
  then {s} c= r" Cl {b} by A6,XBOOLE_1:1;
  then s in r" Cl {b} by ZFMISC_1:31;
  then
A8: r.s in Cl {b} by FUNCT_2:38;
  A c= the carrier of X;
  then reconsider d = r.s as Point of X by TARSKI:def 3;
  {r.s} c= Cl {r.s} by PRE_TOPC:18;
  then
A9: r.s in Cl {r.s} by ZFMISC_1:31;
A10: {a} c= MaxADSet(a) by TEX_4:18;
  r" Cl {r.s} = Cl {d} by A1,Lm2;
  then s in Cl {d} by A9,FUNCT_2:38;
  then MaxADSet(a) c= Cl {d} by A5,TEX_4:23;
  then {a} c= Cl {d} by A10,XBOOLE_1:1;
  then
A11: Cl {a} c= Cl {d} by TOPS_1:5;
  Cl {b} c= Cl {a} by A2,TOPS_3:53;
  then {d} c= Cl {a} by A8,ZFMISC_1:31;
  then Cl {d} c= Cl {a} by TOPS_1:5;
  then Cl {d} = Cl {a} by A11,XBOOLE_0:def 10;
  then
A12: MaxADSet(d) = MaxADSet(a) by TEX_4:49;
  A is maximal_T_0 by Th11;
  then
A13: A is T_0 by Def4;
  r.a = b by A1,A2,BORSUK_1:def 16;
  then A /\ MaxADSet(a) = {b} by A1,Lm3;
  then {b} = {r.s} by A13,A12,Def2;
  then r.s in {b} by ZFMISC_1:31;
  hence contradiction by A4,FUNCT_2:38;
end;

Lm5: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for a being Point of X, b being Point of X0 st a = b holds r" {b} =
MaxADSet(a)
proof
  let r be continuous Function of X,X0;
  assume
A1: r is being_a_retraction;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  let a be Point of X, b be Point of X0;
  assume
A2: a = b;
A3: r" {b} c= MaxADSet(a)
  proof
    assume not r" {b} c= MaxADSet(a);
    then consider s being set such that
A4: s in r" {b} and
A5: not s in MaxADSet(a) by TARSKI:def 3;
    reconsider s as Point of X by A4;
    r.s in {b} by A4,FUNCT_2:38;
    then {r.s} c= {b} by ZFMISC_1:31;
    then {r.s} = {b} by ZFMISC_1:18;
    then A /\ MaxADSet(s) = {b} by A1,Lm3;
    then {a} c= MaxADSet(s) by A2,XBOOLE_1:17;
    then a in MaxADSet(s) by ZFMISC_1:31;
    then
A6: MaxADSet(s) = MaxADSet(a) by TEX_4:21;
    {s} c= MaxADSet(s) by TEX_4:18;
    hence contradiction by A5,A6,ZFMISC_1:31;
  end;
  MaxADSet(a) c= r" {b} by A1,A2,Lm4;
  hence thesis by A3,XBOOLE_0:def 10;
end;

Lm6: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for E being Subset of X, F being Subset of X0 st F = E holds r" F =
MaxADSet(E)
proof
  let r be continuous Function of X,X0;
  assume
A1: r is being_a_retraction;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  let E be Subset of X, F be Subset of X0;
  set R = {MaxADSet(a) where a is Point of X : a in E};
  assume
A2: F = E;
  now
    let x be set;
    assume
A3: x in r" F;
    then reconsider b = x as Point of X;
A4: r.b in F by A3,FUNCT_2:38;
    then reconsider a = r.b as Point of X by A2;
    MaxADSet(a) in R by A2,A4;
    then
A5: MaxADSet(a) c= union R by ZFMISC_1:74;
    A /\ MaxADSet(b) = {a} by A1,Lm3;
    then a in A /\ MaxADSet(b) by ZFMISC_1:31;
    then a in MaxADSet(b) by XBOOLE_0:def 4;
    then
A6: MaxADSet(a) = MaxADSet(b) by TEX_4:21;
    {b} c= MaxADSet(b) by TEX_4:18;
    then b in MaxADSet(a) by A6,ZFMISC_1:31;
    hence x in union R by A5;
  end;
  then
A7: r" F c= union R by TARSKI:def 3;
  A is maximal_T_0 by Th11;
  then
A8: A is T_0 by Def4;
  now
    let C be set;
    assume C in R;
    then consider a being Point of X such that
A9: C = MaxADSet(a) and
A10: a in E;
    now
      let x be set;
      assume
A11:  x in C;
      then reconsider b = x as Point of X by A9;
A12:  A /\ MaxADSet(b) = {r.b} by A1,Lm3;
A13:  A /\ MaxADSet(a) = {a} by A2,A8,A10,Def2;
      MaxADSet(a) = MaxADSet(b) by A9,A11,TEX_4:21;
      then a = r.x by A13,A12,ZFMISC_1:3;
      hence x in r" F by A2,A9,A10,A11,FUNCT_2:38;
    end;
    hence C c= r" F by TARSKI:def 3;
  end;
  then
A14: union R c= r" F by ZFMISC_1:76;
  MaxADSet(E) = union R by TEX_4:def 11;
  hence thesis by A14,A7,XBOOLE_0:def 10;
end;

definition
  let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of
  X;
  func Stone-retraction(X,X0) -> continuous Function of X,X0 means
  :Def9:
  it is being_a_retraction;
  existence by Th22;
  uniqueness
  proof
    reconsider M = the carrier of X0 as non empty Subset of X by TSEP_1:1;
    let r1, r2 be continuous Function of X,X0;
    assume that
A1: r1 is being_a_retraction and
A2: r2 is being_a_retraction;
    for x being set st x in the carrier of X holds r1.x = r2.x
    proof
      let x be set;
      assume x in the carrier of X;
      then reconsider a = x as Point of X;
A3:   M /\ MaxADSet(a) = {r2.a} by A2,Lm3;
      M /\ MaxADSet(a) = {r1.a} by A1,Lm3;
      hence thesis by A3,ZFMISC_1:3;
    end;
    hence r1 = r2 by FUNCT_2:12;
  end;
end;

theorem
  for a being Point of X, b being Point of X0 st a = b holds (
  Stone-retraction(X,X0))" Cl {b} = Cl {a}
proof
  let a be Point of X, b be Point of X0;
  assume
A1: a = b;
  Stone-retraction(X,X0) is being_a_retraction by Def9;
  hence thesis by A1,Lm2;
end;

theorem Th25:
  for a being Point of X, b being Point of X0 st a = b holds (
  Stone-retraction(X,X0))" {b} = MaxADSet(a)
proof
  let a be Point of X, b be Point of X0;
  assume
A1: a = b;
  Stone-retraction(X,X0) is being_a_retraction by Def9;
  hence thesis by A1,Lm5;
end;

theorem Th26:
  for E being Subset of X, F being Subset of X0 st F = E holds (
  Stone-retraction(X,X0))" (F) = MaxADSet(E)
proof
  let E be Subset of X, F be Subset of X0;
  assume
A1: F = E;
  Stone-retraction(X,X0) is being_a_retraction by Def9;
  hence thesis by A1,Lm6;
end;

definition
  let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of
  X;
  redefine func Stone-retraction(X,X0) means
  :
  Def10: for
 M being Subset of X st M = the carrier of X0 for a being Point of X
  holds M /\ MaxADSet(a) = {it.a};
  compatibility
  proof
    reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
    let r be continuous Function of X,X0;
    thus r = Stone-retraction(X,X0) implies for M being Subset of X st M = the
    carrier of X0 for a being Point of X holds M /\ MaxADSet(a) = {r.a}
    proof
      assume
A1:   r = Stone-retraction(X,X0);
      let M be Subset of X;
A2:   Stone-retraction(X,X0) is being_a_retraction by Def9;
      assume M = the carrier of X0;
      hence thesis by A1,A2,Lm3;
    end;
    assume for A being Subset of X st A = the carrier of X0 for a being Point
    of X holds A /\ MaxADSet(a) = {r.a};
    then for a being Point of X holds M /\ MaxADSet(a) = {r.a};
    then r is being_a_retraction by Th20;
    hence r = Stone-retraction(X,X0) by Def9;
  end;
end;

definition
  let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of
  X;
  redefine func Stone-retraction(X,X0) means
  :
  Def11: for a being Point of X holds it.a in MaxADSet(a);
  compatibility
  proof
    reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
    let r be continuous Function of X,X0;
    thus r = Stone-retraction(X,X0) implies for a being Point of X holds r.a
    in MaxADSet(a)
    proof
      assume
A1:   r = Stone-retraction(X,X0);
      let a be Point of X;
      A /\ MaxADSet(a) = {r.a} by A1,Def10;
      then {r.a} c= MaxADSet(a) by XBOOLE_1:17;
      hence thesis by ZFMISC_1:31;
    end;
    assume for a being Point of X holds r.a in MaxADSet(a);
    then r is being_a_retraction by Th21;
    hence r = Stone-retraction(X,X0) by Def9;
  end;
end;

theorem Th27:
  for a being Point of X holds (Stone-retraction(X,X0))" {(
  Stone-retraction(X,X0)).a} = MaxADSet(a)
proof
  let a be Point of X;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
  set r = Stone-retraction(X,X0);
  r.a in A;
  then reconsider b = r.a as Point of X;
A1: r.a in MaxADSet(a) by Def11;
  r" {r.a} = MaxADSet(b) by Th25;
  hence thesis by A1,TEX_4:21;
end;

theorem
  for a being Point of X holds Im(Stone-retraction(X,X0),a) = (
  Stone-retraction(X,X0)).: MaxADSet(a)
proof
  let a be Point of X;
  set r = Stone-retraction(X,X0);
A1: dom r = [#]X by FUNCT_2:def 1;
A2: r.: r" {r.a} c= {r.a} by FUNCT_1:75;
A3: r"{r.a} = MaxADSet(a) by Th27;
  then r.: r" {r.a} <> {} by A1,RELAT_1:119;
  then r.: r" {r.a} = {r.a} by A2,ZFMISC_1:33;
  hence thesis by A1,A3,FUNCT_1:59;
end;

definition
  let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of
  X;
  redefine func Stone-retraction(X,X0) means
  :
  Def12: for
 M being Subset of X st M = the carrier of X0 for A being Subset of X
  holds M /\ MaxADSet(A) = it.: A;
  compatibility
  proof
    let r be continuous Function of X,X0;
    thus r = Stone-retraction(X,X0) implies for M being Subset of X st M = the
    carrier of X0 for A being Subset of X holds M /\ MaxADSet(A) = r.: A
    proof
      assume
A1:   r = Stone-retraction(X,X0);
      let M be Subset of X;
      reconsider N = M as Subset of X;
      assume
A2:   M = the carrier of X0;
      let A be Subset of X;
      N is maximal_T_0 by A2,Th11;
      then
A3:   N is T_0 by Def4;
      for x being set st x in M /\ MaxADSet(A) holds x in r.: A
      proof
        let x be set;
        assume
A4:     x in M /\ MaxADSet(A);
        then reconsider c = x as Point of X;
        c in M by A4,XBOOLE_0:def 4;
        then
A5:     M /\ MaxADSet(c) = {c} by A3,Def2;
        c in MaxADSet(A) by A4,XBOOLE_0:def 4;
        then c in union {MaxADSet(a) where a is Point of X : a in A} by
TEX_4:def 11;
        then consider D being set such that
A6:     c in D and
A7:     D in {MaxADSet(a) where a is Point of X : a in A} by TARSKI:def 4;
        consider a being Point of X such that
A8:     D = MaxADSet(a) and
A9:     a in A by A7;
        MaxADSet(c) = MaxADSet(a) by A6,A8,TEX_4:21;
        then {r.a} = {c} by A1,A2,A5,Def10;
        hence thesis by A9,FUNCT_2:35,ZFMISC_1:3;
      end;
      then
A10:  M /\ MaxADSet(A) c= r.: A by TARSKI:def 3;
      for x being set st x in r.: A holds x in M /\ MaxADSet(A)
      proof
        let x be set;
        assume
A11:    x in r.: A;
        then reconsider b = x as Point of X0;
        consider a being set such that
A12:    a in the carrier of X and
A13:    a in A and
A14:    b = r.a by A11,FUNCT_2:64;
        reconsider a as Point of X by A12;
        {a} c= A by A13,ZFMISC_1:31;
        then MaxADSet({a}) c= MaxADSet(A) by TEX_4:31;
        then MaxADSet(a) c= MaxADSet(A) by TEX_4:28;
        then
A15:    M /\ MaxADSet(a) c= M /\ MaxADSet(A) by XBOOLE_1:26;
        M /\ MaxADSet(a) = {b} by A1,A2,A14,Def10;
        hence thesis by A15,ZFMISC_1:31;
      end;
      then r.: A c= M /\ MaxADSet(A) by TARSKI:def 3;
      hence thesis by A10,XBOOLE_0:def 10;
    end;
    assume
A16: for M being Subset of X st M = the carrier of X0 for A being
    Subset of X holds M /\ MaxADSet(A) = r.: A;
A17: dom r = [#]X by FUNCT_2:def 1;
    for M being Subset of X st M = the carrier of X0 for a being Point of
    X holds M /\ MaxADSet(a) = {r.a}
    proof
      let M be Subset of X;
      assume
A18:  M = the carrier of X0;
      let a be Point of X;
      M /\ MaxADSet({a}) = Im(r,a) by A16,A18;
      then M /\ MaxADSet(a) = Im(r,a) by TEX_4:28;
      hence thesis by A17,FUNCT_1:59;
    end;
    hence r = Stone-retraction(X,X0) by Def10;
  end;
end;

theorem Th29:
  for A being Subset of X holds (Stone-retraction(X,X0))"((
  Stone-retraction(X,X0)).: A) = MaxADSet(A)
proof
  let A be Subset of X;
  reconsider C = the carrier of X0 as non empty Subset of X by TSEP_1:1;
  set r = Stone-retraction(X,X0);
  C c= the carrier of X;
  then reconsider B = r.: A as Subset of X by XBOOLE_1:1;
  C /\ MaxADSet(A) = B by Def12;
  then
A1: B c= MaxADSet(A) by XBOOLE_1:17;
A2: r" (r.: A) = MaxADSet(B) by Th26;
  then A c= MaxADSet(B) by FUNCT_2:42;
  hence thesis by A2,A1,TEX_4:35;
end;

theorem
  for A being Subset of X holds (Stone-retraction(X,X0)).: A = (
  Stone-retraction(X,X0)).: MaxADSet(A)
proof
  let A be Subset of X;
  set r = Stone-retraction(X,X0);
A1: rng r = r.: the carrier of X by RELSET_1:22;
  r.: r" (r.: A) = r.: MaxADSet(A) by Th29;
  hence thesis by A1,FUNCT_1:77,RELAT_1:123;
end;

theorem
  for A, B being Subset of X holds (Stone-retraction(X,X0)).:(A \/ B) =
  (Stone-retraction(X,X0)).:(A) \/ (Stone-retraction(X,X0)).:(B)
proof
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  set r = Stone-retraction(X,X0);
  let A, B be Subset of X;
  r.: (A \/ B) = M /\ (MaxADSet(A \/ B)) by Def12
    .= M /\ (MaxADSet(A) \/ MaxADSet(B)) by TEX_4:36
    .= (M /\ MaxADSet(A)) \/ (M /\ MaxADSet(B)) by XBOOLE_1:23
    .= (r.: A) \/ (M /\ MaxADSet(B)) by Def12
    .= (r.: A) \/ (r.: B) by Def12;
  hence thesis;
end;

theorem
  for A, B being Subset of X st A is open or B is open holds (
  Stone-retraction(X,X0)).:(A /\ B) = (Stone-retraction(X,X0)).:(A) /\ (
  Stone-retraction(X,X0)).:(B)
proof
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  set r = Stone-retraction(X,X0);
  let A, B be Subset of X;
  assume
A1: A is open or B is open;
  r.: (A /\ B) = M /\ (MaxADSet(A /\ B)) by Def12
    .= (M /\ M) /\ (MaxADSet(A) /\ MaxADSet(B)) by A1,TEX_4:65
    .= M /\ (M /\ (MaxADSet(A) /\ MaxADSet(B))) by XBOOLE_1:16
    .= ((M /\ MaxADSet(A)) /\ MaxADSet(B)) /\ M by XBOOLE_1:16
    .= (M /\ MaxADSet(A)) /\ (M /\ MaxADSet(B)) by XBOOLE_1:16
    .= (r.: A) /\ (M /\ MaxADSet(B)) by Def12
    .= (r.: A) /\ (r.: B) by Def12;
  hence thesis;
end;

theorem
  for A, B being Subset of X st A is closed or B is closed holds (
  Stone-retraction(X,X0)).:(A /\ B) = (Stone-retraction(X,X0)).:(A) /\ (
  Stone-retraction(X,X0)).:(B)
proof
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  set r = Stone-retraction(X,X0);
  let A, B be Subset of X;
  assume
A1: A is closed or B is closed;
  r.: (A /\ B) = M /\ (MaxADSet(A /\ B)) by Def12
    .= (M /\ M) /\ (MaxADSet(A) /\ MaxADSet(B)) by A1,TEX_4:64
    .= M /\ (M /\ (MaxADSet(A) /\ MaxADSet(B))) by XBOOLE_1:16
    .= ((M /\ MaxADSet(A)) /\ MaxADSet(B)) /\ M by XBOOLE_1:16
    .= (M /\ MaxADSet(A)) /\ (M /\ MaxADSet(B)) by XBOOLE_1:16
    .= (r.: A) /\ (M /\ MaxADSet(B)) by Def12
    .= (r.: A) /\ (r.: B) by Def12;
  hence thesis;
end;

theorem
  for A being Subset of X holds A is open implies (Stone-retraction(X,X0
  )).:(A) is open
proof
  let A be Subset of X;
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  set B = (Stone-retraction(X,X0)).:(A);
  assume
A1: A is open;
  then A = MaxADSet(A) by TEX_4:56;
  then A /\ M = B by Def12;
  hence thesis by A1,TSP_1:def 1;
end;

theorem
  for A being Subset of X holds A is closed implies (Stone-retraction(X,
  X0)).:(A) is closed
proof
  let A be Subset of X;
  reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
  set B = (Stone-retraction(X,X0)).:(A);
  assume
A1: A is closed;
  then A = MaxADSet(A) by TEX_4:60;
  then A /\ M = B by Def12;
  hence thesis by A1,TSP_1:def 2;
end;