:: Maximal Anti-Discrete Subspaces of Topological Spaces
::  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, ZFMISC_1, SETFAM_1, RCOMP_1,
      TARSKI, STRUCT_0, TOPS_1, TDLAT_3, RELAT_1, TEX_2, TEX_4;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0,
      PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TEX_2;
 constructors SETFAM_1, TOPS_1, TOPS_2, REALSET2, BORSUK_1, TSEP_1, TDLAT_3,
      TEX_1, TEX_2, COMPTS_1;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
      TSEP_1, TEX_1, TEX_2, ZFMISC_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0;
 theorems TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, TOPS_2,
      PCOMPS_1, TSEP_1, TDLAT_3, TEX_2, XBOOLE_0, XBOOLE_1;

begin

:: 1. Properties of the Closure and the Interior Operations.

registration
  let X be non empty TopSpace, A be non empty Subset of X;
  cluster Cl A -> non empty;
  coherence by PCOMPS_1:2;
end;

registration
  let X be TopSpace, A be empty Subset of X;
  cluster Cl A -> empty;
  coherence by PRE_TOPC:22;
end;

registration
  let X be non empty TopSpace, A be non proper Subset of X;
  cluster Cl A -> non proper;
  coherence
  proof
    A = [#]X by SUBSET_1:def 6;
    hence thesis by TOPS_1:2;
  end;
end;

registration
  let X be non trivial TopSpace, A be non trivial Subset of X;
  cluster Cl A -> non trivial;
  coherence
   proof
     A c= Cl A by PRE_TOPC:18;
    hence thesis;
   end;
end;

reserve X for non empty TopSpace;

theorem Th1:
  for A being Subset of X holds Cl A = meet {F where F is Subset of
X: F is closed & A c= F}
proof
  let A be Subset of X;
  set G = {F where F is Subset of X : F is closed & A c= F};
A1: G c= bool the carrier of X
  proof
    let C be set;
    assume C in G;
    then ex P being Subset of X st C = P & P is closed & A c= P;
    hence thesis;
  end;
  [#]X in G;
  then reconsider G as non empty Subset-Family of X by A1;
  now
    let P be set;
    assume P in G;
    then ex F being Subset of X st F = P & F is closed & A c= F;
    hence A c= P;
  end;
  then
A2: A c= meet G by SETFAM_1:5;
  A c= Cl A by PRE_TOPC:18;
  then Cl A in G;
  then
A3: meet G c= Cl A by SETFAM_1:3;
  now
    let S be Subset of X;
    assume S in G;
    then ex F being Subset of X st F = S & F is closed & A c= F;
    hence S is closed;
  end;
  then G is closed by TOPS_2:def 2;
  then Cl A c= meet G by A2,TOPS_1:5,TOPS_2:22;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem Th2:
  for x being Point of X holds Cl {x} = meet {F where F is Subset
  of X : F is closed & x in F}
proof
  let x be Point of X;
  set G = {F where F is Subset of X : F is closed & x in F};
  set H = {F where F is Subset of X : F is closed & {x} c= F};
  now
    let P be set;
    assume P in G;
    then consider F being Subset of X such that
A1: F = P and
A2: F is closed and
A3: x in F;
    {x} c= F by A3,ZFMISC_1:31;
    hence P in H by A1,A2;
  end;
  then
A4: G c= H by TARSKI:def 3;
  now
    let P be set;
    assume P in H;
    then consider F being Subset of X such that
A5: F = P and
A6: F is closed and
A7: {x} c= F;
    x in F by A7,ZFMISC_1:31;
    hence P in G by A5,A6;
  end;
  then
A8: H c= G by TARSKI:def 3;
  Cl {x} = meet H by Th1;
  hence thesis by A4,A8,XBOOLE_0:def 10;
end;

registration
  let X be non empty TopSpace, A be non proper Subset of X;
  cluster Int A -> non proper;
  coherence
  proof
    A = [#]X by SUBSET_1:def 6;
    hence thesis by TOPS_1:15;
  end;
end;

registration
  let X be non empty TopSpace, A be proper Subset of X;
  cluster Int A -> proper;
  coherence
  proof
    now
      assume Int A is non proper;
      then
A1:   Int A = [#]X by SUBSET_1:def 6;
      Int A c= A by TOPS_1:16;
      hence contradiction by A1,XBOOLE_0:def 10;
    end;
    hence thesis;
  end;
end;

registration
  let X be non empty TopSpace, A be empty Subset of X;
  cluster Int A -> empty;
  coherence;
end;

theorem
  for A being Subset of X holds Int A = union {G where G is Subset of X
  : G is open & G c= A}
proof
  let A be Subset of X;
  set F = {G where G is Subset of X : G is open & G c= A};
A1: F c= bool the carrier of X
  proof
    let C be set;
    assume C in F;
    then ex P being Subset of X st C = P & P is open & P c= A;
    hence thesis;
  end;
  {} c= A by XBOOLE_1:2;
  then {}X in F;
  then reconsider F as non empty Subset-Family of X by A1;
  now
    let P be set;
    assume P in F;
    then ex G being Subset of X st G = P & G is open & G c= A;
    hence P c= A;
  end;
  then
A2: union F c= A by ZFMISC_1:76;
  Int A c= A by TOPS_1:16;
  then Int A in F;
  then
A3: Int A c= union F by ZFMISC_1:74;
  now
    let S be Subset of X;
    assume S in F;
    then ex G being Subset of X st G = S & G is open & G c= A;
    hence S is open;
  end;
  then F is open by TOPS_2:def 1;
  then union F c= Int A by A2,TOPS_1:24,TOPS_2:19;
  hence thesis by A3,XBOOLE_0:def 10;
end;

begin

:: 2. Anti-discrete Subsets of Topological Structures.

definition
  let Y be TopStruct;
  let IT be Subset of Y;
  attr IT is anti-discrete means
  :Def1:
  for x being Point of Y, G being Subset
  of Y st G is open & x in G holds x in IT implies IT c= G;
end;

definition
  let Y be non empty TopStruct;
  let A be Subset of Y;
  redefine attr A is anti-discrete means
  :Def2:
  for x being Point of Y, F
  being Subset of Y st F is closed & x in F holds x in A implies A c= F;
  compatibility
  proof
    hereby
      assume
A1:   A is anti-discrete;
      let x be Point of Y, F be Subset of Y;
      set G = [#]Y \ F;
A2:   A \ F c= G by XBOOLE_1:33;
      assume F is closed;
      then
A3:   G is open by PRE_TOPC:def 3;
      assume
A4:   x in F;
      assume
A5:   x in A;
      assume not A c= F;
      then A \ F <> {} by XBOOLE_1:37;
      then consider a being set such that
A6:   a in A \ F by XBOOLE_0:def 1;
      a in A by A6,XBOOLE_0:def 5;
      then A c= G by A1,A6,A2,A3,Def1;
      then
A7:   A misses G` by SUBSET_1:24;
A8:   G` = (F`)` .= F;
      A /\ F is non empty by A4,A5,XBOOLE_0:def 4;
      hence contradiction by A8,A7,XBOOLE_0:def 7;
    end;
    hereby
      assume
A9:   for x being Point of Y, F being Subset of Y st F is closed & x
      in F holds x in A implies A c= F;
      now
        let x be Point of Y, G be Subset of Y;
        set F = [#]Y \ G;
A10:    A \ G c= F by XBOOLE_1:33;
A11:    G = [#]Y \ F by PRE_TOPC:3;
        assume G is open;
        then
A12:    F is closed by A11,PRE_TOPC:def 3;
        assume
A13:    x in G;
        assume
A14:    x in A;
        assume not A c= G;
        then A \ G <> {} by XBOOLE_1:37;
        then consider a being set such that
A15:    a in A \ G by XBOOLE_0:def 1;
A16:    F = G`;
        a in A by A15,XBOOLE_0:def 5;
        then A c= F by A9,A15,A10,A12;
        then A misses F` by SUBSET_1:24;
        hence contradiction by A13,A14,A16,XBOOLE_0:3;
      end;
      hence A is anti-discrete by Def1;
    end;
  end;
end;

definition
  let Y be TopStruct;
  let A be Subset of Y;
  redefine attr A is anti-discrete means
  :Def3:
  for G being Subset of Y st G is open holds A misses G or A c= G;
  compatibility
  proof
    hereby
      assume
A1:   A is anti-discrete;
      let G be Subset of Y;
      assume
A2:   G is open;
      assume A meets G;
      then consider a being set such that
A3:   a in A /\ G by XBOOLE_0:4;
      reconsider a as Point of Y by A3;
A4:   a in G by A3,XBOOLE_0:def 4;
      a in A by A3,XBOOLE_0:def 4;
      hence A c= G by A1,A2,A4,Def1;
    end;
    assume
A5: for G being Subset of Y st G is open holds A misses G or A c= G;
    now
      let x be Point of Y, G be Subset of Y;
      assume
A6:   G is open;
      assume
A7:   x in G;
      assume x in A;
      then A meets G by A7,XBOOLE_0:3;
      hence A c= G by A5,A6;
    end;
    hence thesis by Def1;
  end;
end;

definition
  let Y be TopStruct;
  let A be Subset of Y;
  redefine attr A is anti-discrete means
  :Def4:
  for F being Subset of Y st F is closed holds A misses F or A c= F;
  compatibility
  proof
    hereby
      assume
A1:   A is anti-discrete;
      let G be Subset of Y;
      assume G is closed;
      then [#]Y \ G is open by PRE_TOPC:def 3;
      then
A2:   A misses G` or A c= G` by A1,Def3;
      assume A meets G;
      then A c= (G`)` by A2,SUBSET_1:23;
      hence A c= G;
    end;
    hereby
      assume
A3:   for G being Subset of Y st G is closed holds A misses G or A c= G;
      now
        let G be Subset of Y;
A4:     G = [#]Y \ ([#]Y \ G) by PRE_TOPC:3;
        assume G is open;
        then [#]Y \ G is closed by A4,PRE_TOPC:def 3;
        then
A5:     A misses G` or A c= G` by A3;
        assume A meets G;
        then A c= G`` by A5,SUBSET_1:23;
        hence A c= G;
      end;
      hence A is anti-discrete by Def3;
    end;
  end;
end;

theorem Th4:
  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
  anti-discrete implies D1 is anti-discrete
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 anti-discrete;
  now
    let D be Subset of Y1;
    reconsider E = D as Subset of Y0 by A1;
    assume D is open;
    then E in the topology of Y0 by A1,PRE_TOPC:def 2;
    then E is open by PRE_TOPC:def 2;
    hence D1 misses D or D1 c= D by A2,A3,Def3;
  end;
  hence thesis by Def3;
end;

reserve Y for non empty TopStruct;

theorem Th5:
  for A, B being Subset of Y st B c= A holds A is anti-discrete
  implies B is anti-discrete
proof
  let A, B be Subset of Y;
  assume
A1: B c= A;
  assume
A2: A is anti-discrete;
  now
    let G be Subset of Y;
    assume
A3: G is open;
    assume B meets G;
    then B /\ G <> {} by XBOOLE_0:def 7;
    then A /\ G <> {} by A1,XBOOLE_1:3,26;
    then A meets G by XBOOLE_0:def 7;
    then A c= G by A2,A3,Def3;
    hence B c= G by A1,XBOOLE_1:1;
  end;
  hence thesis by Def3;
end;

theorem Th6:
  for x being Point of Y holds {x} is anti-discrete
proof
  let x be Point of Y;
  now
    let G be Subset of Y such that
    G is open;
    assume {x} meets G;
    then consider a being set such that
A1: a in {x} /\ G by XBOOLE_0:4;
    a in {x} by A1,XBOOLE_0:def 4;
    then
A2: a = x by TARSKI:def 1;
    a in G by A1,XBOOLE_0:def 4;
    hence {x} c= G by A2,ZFMISC_1:31;
  end;
  hence thesis by Def3;
end;

theorem Th7:
  for A being empty Subset of Y holds A is anti-discrete
proof
  let A be empty Subset of Y;
  for G be Subset of Y st G is open holds A misses G or A c= G by XBOOLE_1:65;
  hence thesis by Def3;
end;

definition
  let Y be TopStruct;
  let IT be Subset-Family of Y;
  attr IT is anti-discrete-set-family means
  :Def5:
  for A being Subset of Y st A in IT holds A is anti-discrete;
end;

theorem Th8:
  for F being Subset-Family of Y st F is anti-discrete-set-family
  holds meet F <> {} implies union F is anti-discrete
proof
  let F be Subset-Family of Y;
  assume
A1: F is anti-discrete-set-family;
  assume
A2: meet F <> {};
  for G being Subset of Y st G is open holds (union F) misses G or union F c= G
  proof
    let G be Subset of Y;
    assume
A3: G is open;
    assume union F meets G;
    then consider A0 being set such that
A4: A0 in F and
A5: A0 meets G by ZFMISC_1:80;
    reconsider A0 as Subset of Y by A4;
    A0 is anti-discrete by A1,A4,Def5;
    then
A6: A0 c= G by A3,A5,Def3;
    meet F c= A0 by A4,SETFAM_1:3;
    then
A7: meet F c= G by A6,XBOOLE_1:1;
    for B being set st B in F holds B c= G
    proof
      let B be set;
      assume
A8:   B in F;
      then reconsider B0 = B as Subset of Y;
      meet F c= B0 by A8,SETFAM_1:3;
      then B0 /\ G <> {} by A2,A7,XBOOLE_1:3,19;
      then
A9:   B0 meets G by XBOOLE_0:def 7;
      B0 is anti-discrete by A1,A8,Def5;
      hence thesis by A3,A9,Def3;
    end;
    hence thesis by ZFMISC_1:76;
  end;
  hence thesis by Def3;
end;

theorem
  for F being Subset-Family of Y st F is anti-discrete-set-family holds
  meet F is anti-discrete
proof
  let F be Subset-Family of Y;
  assume
A1: F is anti-discrete-set-family;
  hereby
    per cases;
    suppose
      meet F = {};
      hence thesis by Th7;
    end;
    suppose
A2:   meet F <> {};
      meet F c= union F by SETFAM_1:2;
      hence thesis by A1,A2,Th5,Th8;
    end;
  end;
end;

definition
  let Y be TopStruct, x be Point of Y;
  func MaxADSF(x) -> Subset-Family of Y equals
  {A where A is Subset of Y : A
  is anti-discrete & x in A};
  coherence
  proof
    set F = {A where A is Subset of Y : A is anti-discrete & x in A};
    F c= bool the carrier of Y
    proof
      let C be set;
      assume C in F;
      then ex A being Subset of Y st C = A & A is anti-discrete & x in A;
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  let Y be non empty TopStruct, x be Point of Y;
  cluster MaxADSF(x) -> non empty;
  coherence
  proof
    set F = {A where A is Subset of Y : A is anti-discrete & x in A};
A1: x in {x} by TARSKI:def 1;
    {x} is anti-discrete by Th6;
    then {x} in F by A1;
    hence thesis;
  end;
end;

reserve x for Point of Y;

theorem Th10:
  MaxADSF(x) is anti-discrete-set-family
proof
  now
    let A be Subset of Y;
    assume A in MaxADSF(x);
    then ex C being Subset of Y st C = A & C is anti-discrete & x in C;
    hence A is anti-discrete;
  end;
  hence thesis by Def5;
end;

theorem Th11:
  {x} = meet MaxADSF(x)
proof
A1: x in {x} by TARSKI:def 1;
  now
    let A be set;
    assume A in MaxADSF(x);
    then ex C being Subset of Y st C = A & C is anti-discrete & x in C;
    hence {x} c= A by ZFMISC_1:31;
  end;
  then
A2: {x} c= meet MaxADSF(x) by SETFAM_1:5;
  {x} is anti-discrete by Th6;
  then {x} in MaxADSF(x) by A1;
  then meet MaxADSF(x) c= {x} by SETFAM_1:3;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem Th12:
  {x} c= union MaxADSF(x)
proof
  {x} = meet MaxADSF(x) by Th11;
  hence thesis by SETFAM_1:2;
end;

theorem Th13:
  union MaxADSF(x) is anti-discrete
proof
  {x} = meet MaxADSF(x) by Th11;
  hence thesis by Th8,Th10;
end;

begin

:: 3. Maximal Anti-discrete Subsets of Topological Structures.

definition
  let Y be TopStruct;
  let IT be Subset of Y;
  attr IT is maximal_anti-discrete means
  :Def7:
  IT is anti-discrete & for D
  being Subset of Y st D is anti-discrete & 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_anti-discrete implies D1 is maximal_anti-discrete
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_anti-discrete;
A4: now
    let D be Subset of Y1;
    reconsider E = D as Subset of Y0 by A1;
    assume D is anti-discrete;
    then
A5: E is anti-discrete by A1,Th4;
    assume D1 c= D;
    hence D1 = D by A2,A3,A5,Def7;
  end;
  D0 is anti-discrete by A3,Def7;
  then D1 is anti-discrete by A1,A2,Th4;
  hence thesis by A4,Def7;
end;

reserve Y for non empty TopStruct;

theorem Th15:
  for A being empty Subset of Y holds A is not maximal_anti-discrete
proof
  consider a being set such that
A1: a in the carrier of Y by XBOOLE_0:def 1;
  reconsider a as Point of Y by A1;
  let A be empty Subset of Y;
  now
    take C = {a};
    thus C is anti-discrete & A c= C & A <> C by Th6,XBOOLE_1:2;
  end;
  hence thesis by Def7;
end;

theorem Th16:
  for A being non empty Subset of Y holds A is anti-discrete & A
  is open implies A is maximal_anti-discrete
proof
  let A be non empty Subset of Y;
  assume
A1: A is anti-discrete;
  assume
A2: A is open;
  for D being Subset of Y st D is anti-discrete & A c= D holds A = D
  proof
    let D be Subset of Y;
    assume D is anti-discrete;
    then D misses A or D c= A by A2,Def3;
    then
A3: D /\ A = {} or D c= A by XBOOLE_0:def 7;
    assume A c= D;
    hence thesis by A3,XBOOLE_0:def 10,XBOOLE_1:28;
  end;
  hence thesis by A1,Def7;
end;

theorem Th17:
  for A being non empty Subset of Y holds A is anti-discrete & A
  is closed implies A is maximal_anti-discrete
proof
  let A be non empty Subset of Y;
  assume
A1: A is anti-discrete;
  assume
A2: A is closed;
  for D being Subset of Y st D is anti-discrete & A c= D holds A = D
  proof
    let D be Subset of Y;
    assume D is anti-discrete;
    then D misses A or D c= A by A2,Def4;
    then
A3: D /\ A = {} or D c= A by XBOOLE_0:def 7;
    assume A c= D;
    hence thesis by A3,XBOOLE_0:def 10,XBOOLE_1:28;
  end;
  hence thesis by A1,Def7;
end;

definition
  let Y be TopStruct, x be Point of Y;
  func MaxADSet(x) -> Subset of Y equals
  union MaxADSF(x);
  coherence;
end;

registration
  let Y be non empty TopStruct, x be Point of Y;
  cluster MaxADSet(x) -> non empty;
  coherence
  proof
    {x} c= union MaxADSF(x) by Th12;
    hence thesis;
  end;
end;

theorem
  for x being Point of Y holds {x} c= MaxADSet(x) by Th12;

theorem Th19:
  for D being Subset of Y, x being Point of Y st D is
  anti-discrete & x in D holds D c= MaxADSet(x)
proof
  let D be Subset of Y, x be Point of Y;
  assume
A1: D is anti-discrete;
  assume x in D;
  then D in {A where A is Subset of Y : A is anti-discrete & x in A} by A1;
  hence thesis by ZFMISC_1:74;
end;

theorem Th20:
  for x being Point of Y holds MaxADSet(x) is maximal_anti-discrete
proof
  let x be Point of Y;
A1: for D being Subset of Y st D is anti-discrete & MaxADSet(x) c= D holds
  MaxADSet(x) = D
  proof
    let D be Subset of Y;
    assume
A2: D is anti-discrete;
    assume
A3: MaxADSet(x) c= D;
    {x} c= MaxADSet(x) by Th12;
    then {x} c= D by A3,XBOOLE_1:1;
    then x in D by ZFMISC_1:31;
    then D c= MaxADSet(x) by A2,Th19;
    hence thesis by A3,XBOOLE_0:def 10;
  end;
  MaxADSet(x) is anti-discrete by Th13;
  hence thesis by A1,Def7;
end;

theorem Th21:
  for x, y being Point of Y holds y in MaxADSet(x) iff MaxADSet(y)
  = MaxADSet(x)
proof
  let x, y be Point of Y;
  MaxADSet(y) is maximal_anti-discrete by Th20;
  then
A1: MaxADSet(y) is anti-discrete by Def7;
A2: MaxADSet(x) is maximal_anti-discrete by Th20;
  then
A3: MaxADSet(x) is anti-discrete by Def7;
  thus y in MaxADSet(x) implies MaxADSet(y) = MaxADSet(x)
  proof
    assume y in MaxADSet(x);
    then
    MaxADSet(x) in {A where A is Subset of Y : A is anti-discrete & y in A
    } by A3;
    then MaxADSet(x) c= MaxADSet(y) by ZFMISC_1:74;
    hence thesis by A2,A1,Def7;
  end;
  assume
A4: MaxADSet(y) = MaxADSet(x);
  {y} c= MaxADSet(y) by Th12;
  hence thesis by A4,ZFMISC_1:31;
end;

theorem Th22:
  for x, y being Point of Y holds MaxADSet(x) misses MaxADSet(y)
  or MaxADSet(x) = MaxADSet(y)
proof
  let x, y be Point of Y;
  assume MaxADSet(x) /\ MaxADSet(y) <> {};
  then consider a being set such that
A1: a in MaxADSet(x) /\ MaxADSet(y) by XBOOLE_0:def 1;
  reconsider a as Point of Y by A1;
  a in MaxADSet(x) by A1,XBOOLE_0:def 4;
  then
A2: MaxADSet(a) = MaxADSet(x) by Th21;
  a in MaxADSet(y) by A1,XBOOLE_0:def 4;
  hence thesis by A2,Th21;
end;

theorem Th23:
  for F being Subset of Y, x being Point of Y st F is closed & x
  in F holds MaxADSet(x) c= F
proof
  let F be Subset of Y, x be Point of Y;
  assume that
A1: F is closed and
A2: x in F;
  {x} c= MaxADSet(x) by Th12;
  then
A3: x in MaxADSet(x) by ZFMISC_1:31;
  MaxADSet(x) is maximal_anti-discrete by Th20;
  then MaxADSet(x) is anti-discrete by Def7;
  hence thesis by A1,A2,A3,Def2;
end;

theorem Th24:
  for G being Subset of Y, x being Point of Y st G is open & x in
  G holds MaxADSet(x) c= G
proof
  let G be Subset of Y, x be Point of Y;
  assume that
A1: G is open and
A2: x in G;
  {x} c= MaxADSet(x) by Th12;
  then
A3: x in MaxADSet(x) by ZFMISC_1:31;
  MaxADSet(x) is maximal_anti-discrete by Th20;
  then MaxADSet(x) is anti-discrete by Def7;
  hence thesis by A1,A2,A3,Def1;
end;

theorem
  for x being Point of Y holds MaxADSet(x) c= meet {F where F is Subset
  of Y : F is closed & x in F}
proof
  let x be Point of Y;
  set G = {F where F is Subset of Y : F is closed & x in F};
  G c= bool the carrier of Y
  proof
    let C be set;
    assume C in G;
    then ex P being Subset of Y st C = P & P is closed & x in P;
    hence thesis;
  end;
  then reconsider G as Subset-Family of Y;
  now
    let C be set;
    assume C in G;
    then ex F being Subset of Y st F = C & F is closed & x in F;
    hence MaxADSet(x) c= C by Th23;
  end;
  hence thesis by SETFAM_1:5;
end;

theorem
  for x being Point of Y holds MaxADSet(x) c= meet {G where G is Subset
  of Y : G is open & x in G}
proof
  let x be Point of Y;
  set F = {G where G is Subset of Y : G is open & x in G};
  F c= bool the carrier of Y
  proof
    let C be set;
    assume C in F;
    then ex P being Subset of Y st C = P & P is open & x in P;
    hence thesis;
  end;
  then reconsider F as Subset-Family of Y;
  now
    let C be set;
    assume C in F;
    then ex G being Subset of Y st G = C & G is open & x in G;
    hence MaxADSet(x) c= C by Th24;
  end;
  hence thesis by SETFAM_1:5;
end;

definition
  let Y be non empty TopStruct;
  let A be Subset of Y;
  redefine attr A is maximal_anti-discrete means
  :Def9:
  ex x being Point of Y st x in A & A = MaxADSet(x);
  compatibility
  proof
    thus A is maximal_anti-discrete implies ex x being Point of Y st x in A &
    A = MaxADSet(x)
    proof
      assume
A1:   A is maximal_anti-discrete;
      then A <> {} by Th15;
      then consider x being set such that
A2:   x in A by XBOOLE_0:def 1;
      reconsider x as Point of Y by A2;
      take x;
      thus x in A by A2;
      MaxADSet(x) is maximal_anti-discrete by Th20;
      then
A3:   MaxADSet(x) is anti-discrete by Def7;
      A is anti-discrete by A1,Def7;
      then A c= MaxADSet(x) by A2,Th19;
      hence thesis by A1,A3,Def7;
    end;
    assume ex x being Point of Y st x in A & A = MaxADSet(x);
    hence thesis by Th20;
  end;
end;

theorem Th27:
  for A being Subset of Y, x being Point of Y st x in A holds A is
  maximal_anti-discrete implies A = MaxADSet(x)
proof
  let A be Subset of Y, x be Point of Y;
  assume
A1: x in A;
  assume A is maximal_anti-discrete;
  then ex y being Point of Y st y in A & A = MaxADSet(y) by Def9;
  hence thesis by A1,Th21;
end;

definition
  let Y be non empty TopStruct;
  let A be non empty Subset of Y;
  redefine attr A is maximal_anti-discrete means
  for x being Point of Y st x in A holds A = MaxADSet(x);
  compatibility
  proof
    thus A is maximal_anti-discrete implies for x being Point of Y st x in A
    holds A = MaxADSet(x) by Th27;
    consider a being set such that
A1: a in A by XBOOLE_0:def 1;
    reconsider a as Point of Y by A1;
    assume
A2: for x being Point of Y st x in A holds A = MaxADSet(x);
    now
      take a;
      thus a in A by A1;
      thus A = MaxADSet(a) by A2,A1;
    end;
    hence thesis by Def9;
  end;
end;

definition
  let Y be non empty TopStruct, A be Subset of Y;
  func MaxADSet(A) -> Subset of Y equals
  union {MaxADSet(a) where a is Point
  of Y : a in A};
  coherence
  proof
    set M = {MaxADSet(a) where a is Point of Y : a in A};
    M c= bool the carrier of Y
    proof
      let C be set;
      assume C in M;
      then ex a being Point of Y st C = MaxADSet(a) & a in A;
      hence thesis;
    end;
    then reconsider M as Subset-Family of Y;
    union M is Subset of Y;
    hence thesis;
  end;
end;

theorem Th28:
  for x being Point of Y holds MaxADSet(x) = MaxADSet({x})
proof
  let x be Point of Y;
  set M = {MaxADSet(a) where a is Point of Y : a in {x}};
  now
    let P be set;
    assume P in M;
    then ex a being Point of Y st P = MaxADSet(a) & a in {x};
    hence P c= MaxADSet(x) by TARSKI:def 1;
  end;
  then
A1: MaxADSet({x}) c= MaxADSet(x) by ZFMISC_1:76;
  x in {x} by TARSKI:def 1;
  then MaxADSet(x) in M;
  then MaxADSet(x) c= MaxADSet({x}) by ZFMISC_1:74;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th29:
  for A being Subset of Y, x being Point of Y holds MaxADSet(x)
  meets MaxADSet(A) implies MaxADSet(x) meets A
proof
  let A be Subset of Y, x be Point of Y;
  set E = {MaxADSet(a) where a is Point of Y : a in A};
  assume MaxADSet(x) /\ MaxADSet(A) <> {};
  then consider z being set such that
A1: z in MaxADSet(x) /\ MaxADSet(A) by XBOOLE_0:def 1;
  reconsider z as Point of Y by A1;
  z in MaxADSet(A) by A1,XBOOLE_0:def 4;
  then consider C being set such that
A2: z in C and
A3: C in E by TARSKI:def 4;
  z in MaxADSet(x) by A1,XBOOLE_0:def 4;
  then
A4: MaxADSet(z) = MaxADSet(x) by Th21;
  consider b being Point of Y such that
A5: C = MaxADSet(b) and
A6: b in A by A3;
  MaxADSet(b) = MaxADSet(z) by A2,A5,Th21;
  then {b} c= MaxADSet(x) by A4,Th12;
  then b in MaxADSet(x) by ZFMISC_1:31;
  hence thesis by A6,XBOOLE_0:3;
end;

theorem Th30:
  for A being Subset of Y, x being Point of Y holds MaxADSet(x)
  meets MaxADSet(A) implies MaxADSet(x) c= MaxADSet(A)
proof
  let A be Subset of Y, x be Point of Y;
  set F = {MaxADSet(b) where b is Point of Y : b in A};
  assume MaxADSet(x) meets MaxADSet(A);
  then MaxADSet(x) meets A by Th29;
  then consider z being set such that
A1: z in MaxADSet(x) /\ A by XBOOLE_0:4;
  reconsider z as Point of Y by A1;
  set E = {MaxADSet(a) where a is Point of Y : a in {z}};
  z in A by A1,XBOOLE_0:def 4;
  then
A2: {z} c= A by ZFMISC_1:31;
  E c= F
  proof
    let C be set;
    assume C in E;
    then ex a being Point of Y st C = MaxADSet(a) & a in {z};
    hence thesis by A2;
  end;
  then MaxADSet({z}) c= MaxADSet(A) by ZFMISC_1:77;
  then
A3: MaxADSet(z) c= MaxADSet(A) by Th28;
  z in MaxADSet(x) by A1,XBOOLE_0:def 4;
  hence thesis by A3,Th21;
end;

theorem Th31:
  for A, B being Subset of Y holds A c= B implies MaxADSet(A) c= MaxADSet(B)
proof
  let A, B be Subset of Y;
  set E = {MaxADSet(a) where a is Point of Y : a in A};
  set F = {MaxADSet(b) where b is Point of Y : b in B};
  assume
A1: A c= B;
  E c= F
  proof
    let C be set;
    assume C in E;
    then ex a being Point of Y st C = MaxADSet(a) & a in A;
    hence thesis by A1;
  end;
  hence thesis by ZFMISC_1:77;
end;

theorem Th32:
  for A being Subset of Y holds A c= MaxADSet(A)
proof
  let A be Subset of Y;
  now
    let x be set;
    assume
A1: x in A;
    then reconsider a = x as Point of Y;
    {a} c= A by A1,ZFMISC_1:31;
    then MaxADSet({a}) c= MaxADSet(A) by Th31;
    then
A2: MaxADSet(a) c= MaxADSet(A) by Th28;
A3: a in {a} by TARSKI:def 1;
    {a} c= MaxADSet(a) by Th12;
    then {a} c= MaxADSet(A) by A2,XBOOLE_1:1;
    hence x in MaxADSet(A) by A3;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th33:
  for A being Subset of Y holds MaxADSet(A) = MaxADSet(MaxADSet(A) )
proof
  let A be Subset of Y;
A1: MaxADSet(MaxADSet(A)) c= MaxADSet(A)
  proof
    let x be set;
    assume x in MaxADSet(MaxADSet(A));
    then consider C being set such that
A2: x in C and
A3: C in {MaxADSet(a) where a is Point of Y : a in MaxADSet(A)} by TARSKI:def 4
;
    consider a being Point of Y such that
A4: C = MaxADSet(a) and
A5: a in MaxADSet(A) by A3;
    consider D being set such that
A6: a in D and
A7: D in {MaxADSet(b) where b is Point of Y : b in A} by A5,TARSKI:def 4;
    consider b being Point of Y such that
A8: D = MaxADSet(b) and
    b in A by A7;
    MaxADSet(a) = MaxADSet(b) by A6,A8,Th21;
    hence thesis by A2,A4,A7,A8,TARSKI:def 4;
  end;
  MaxADSet(A) c= MaxADSet(MaxADSet(A)) by Th32;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th34:
  for A, B being Subset of Y holds A c= MaxADSet(B) implies
  MaxADSet(A) c= MaxADSet(B)
proof
  let A, B be Subset of Y;
  assume A c= MaxADSet(B);
  then MaxADSet(A) c= MaxADSet(MaxADSet(B)) by Th31;
  hence thesis by Th33;
end;

theorem Th35:
  for A, B being Subset of Y st B c= MaxADSet(A) & A c= MaxADSet(B
  ) holds MaxADSet(A) = MaxADSet(B)
proof
  let A, B be Subset of Y;
  thus B c= MaxADSet(A) & A c= MaxADSet(B) implies MaxADSet(A) = MaxADSet(B)
  proof
    assume that
A1: B c= MaxADSet(A) and
A2: A c= MaxADSet(B);
A3: MaxADSet(A) c= MaxADSet(B) by A2,Th34;
    MaxADSet(B) c= MaxADSet(A) by A1,Th34;
    hence thesis by A3,XBOOLE_0:def 10;
  end;
end;

theorem
  for A, B being Subset of Y holds MaxADSet(A \/ B) = MaxADSet(A) \/
  MaxADSet(B)
proof
  let A, B be Subset of Y;
A1: MaxADSet(A \/ B) c= MaxADSet(A) \/ MaxADSet(B)
  proof
    let x be set;
    assume x in MaxADSet(A \/ B);
    then consider C being set such that
A2: x in C and
A3: C in {MaxADSet(a) where a is Point of Y : a in A \/ B} by TARSKI:def 4;
    consider a being Point of Y such that
A4: C = MaxADSet(a) and
A5: a in A \/ B by A3;
    now
      per cases by A5,XBOOLE_0:def 3;
      suppose
A6:     a in A;
        now
          take C;
          thus x in C by A2;
          thus C in {MaxADSet(c) where c is Point of Y : c in A} by A4,A6;
        end;
        then
A7:     x in MaxADSet(A) by TARSKI:def 4;
        MaxADSet(A) c= MaxADSet(A) \/ MaxADSet(B) by XBOOLE_1:7;
        hence thesis by A7;
      end;
      suppose
A8:     a in B;
        now
          take C;
          thus x in C by A2;
          thus C in {MaxADSet(c) where c is Point of Y : c in B} by A4,A8;
        end;
        then
A9:     x in MaxADSet(B) by TARSKI:def 4;
        MaxADSet(B) c= MaxADSet(A) \/ MaxADSet(B) by XBOOLE_1:7;
        hence thesis by A9;
      end;
    end;
    hence thesis;
  end;
A10: MaxADSet(B) c= MaxADSet(A \/ B) by Th31,XBOOLE_1:7;
  MaxADSet(A) c= MaxADSet(A \/ B) by Th31,XBOOLE_1:7;
  then MaxADSet(A) \/ MaxADSet(B) c= MaxADSet(A \/ B) by A10,XBOOLE_1:8;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th37:
  for A, B being Subset of Y holds MaxADSet(A /\ B) c= MaxADSet(A)
  /\ MaxADSet(B)
proof
  let A, B be Subset of Y;
A1: MaxADSet(A /\ B) c= MaxADSet(B) by Th31,XBOOLE_1:17;
  MaxADSet(A /\ B) c= MaxADSet(A) by Th31,XBOOLE_1:17;
  hence thesis by A1,XBOOLE_1:19;
end;

registration
  let Y be non empty TopStruct, A be non empty Subset of Y;
  cluster MaxADSet(A) -> non empty;
  coherence by Th32,XBOOLE_1:3;
end;

registration
  let Y be non empty TopStruct, A be empty Subset of Y;
  cluster MaxADSet(A) -> empty;
  coherence
  proof
    now
      assume MaxADSet(A) is non empty;
      then consider x being set such that
A1:   x in MaxADSet(A) by XBOOLE_0:def 1;
      reconsider a = x as Point of Y by A1;
      consider D being set such that
      a in D and
A2:   D in {MaxADSet(b) where b is Point of Y : b in A} by A1,TARSKI:def 4;
      ex b being Point of Y st D = MaxADSet(b) & b in A by A2;
      hence contradiction;
    end;
    hence thesis;
  end;
end;

registration
  let Y be non empty TopStruct, A be non proper Subset of Y;
  cluster MaxADSet(A) -> non proper;
  coherence
  proof
    A = the carrier of Y by SUBSET_1:def 6;
    then the carrier of Y c= MaxADSet(A) by Th32;
    then MaxADSet(A) = the carrier of Y by XBOOLE_0:def 10;
    hence thesis by SUBSET_1:def 6;
  end;
end;

registration
  let Y be non trivial TopStruct, A be non trivial Subset of Y;
  cluster MaxADSet(A) -> non trivial;
  coherence
   proof
     A c= MaxADSet(A) by Th32;
    hence thesis;
   end;
end;

theorem Th38:
  for G being Subset of Y, A being Subset of Y st G is open & A c=
  G holds MaxADSet(A) c= G
proof
  let G be Subset of Y, A be Subset of Y;
  assume
A1: G is open;
  assume
A2: A c= G;
  MaxADSet(A) c= G
  proof
    let x be set;
    assume
A3: x in MaxADSet(A);
    then reconsider a = x as Point of Y;
    consider D being set such that
A4: a in D and
A5: D in {MaxADSet(b) where b is Point of Y : b in A} by A3,TARSKI:def 4;
    consider b being Point of Y such that
A6: D = MaxADSet(b) and
A7: b in A by A5;
A8: MaxADSet(a) = MaxADSet(b) by A4,A6,Th21;
A9: {a} c= MaxADSet(a) by Th12;
    MaxADSet(b) c= G by A1,A2,A7,Th24;
    then {a} c= G by A8,A9,XBOOLE_1:1;
    hence thesis by ZFMISC_1:31;
  end;
  hence thesis;
end;

theorem Th39:
  for A being Subset of Y holds {G where G is Subset of Y : G is
open & A c= G} <> {} implies MaxADSet(A) c= meet {G where G is Subset of Y : G
  is open & A c= G}
proof
  let A be Subset of Y;
  set F = {G where G is Subset of Y : G is open & A c= G};
  F c= bool the carrier of Y
  proof
    let C be set;
    assume C in F;
    then ex P being Subset of Y st C = P & P is open & A c= P;
    hence thesis;
  end;
  then reconsider F as Subset-Family of Y;
A1: now
    let C be set;
    assume C in F;
    then ex G being Subset of Y st G = C & G is open & A c= G;
    hence MaxADSet(A) c= C by Th38;
  end;
  assume {G where G is Subset of Y : G is open & A c= G} <> {};
  hence thesis by A1,SETFAM_1:5;
end;

theorem Th40:
  for F being Subset of Y, A being Subset of Y st F is closed & A
  c= F holds MaxADSet(A) c= F
proof
  let F be Subset of Y, A be Subset of Y;
  assume
A1: F is closed;
  assume
A2: A c= F;
  MaxADSet(A) c= F
  proof
    let x be set;
    assume
A3: x in MaxADSet(A);
    then reconsider a = x as Point of Y;
    consider D being set such that
A4: a in D and
A5: D in {MaxADSet(b) where b is Point of Y : b in A} by A3,TARSKI:def 4;
    consider b being Point of Y such that
A6: D = MaxADSet(b) and
A7: b in A by A5;
A8: MaxADSet(a) = MaxADSet(b) by A4,A6,Th21;
A9: {a} c= MaxADSet(a) by Th12;
    MaxADSet(b) c= F by A1,A2,A7,Th23;
    then {a} c= F by A8,A9,XBOOLE_1:1;
    hence thesis by ZFMISC_1:31;
  end;
  hence thesis;
end;

theorem Th41:
  for A being Subset of Y holds {F where F is Subset of Y : F is
closed & A c= F} <> {} implies MaxADSet(A) c= meet {F where F is Subset of Y :
  F is closed & A c= F}
proof
  let A be Subset of Y;
  set G = {F where F is Subset of Y : F is closed & A c= F};
  G c= bool the carrier of Y
  proof
    let C be set;
    assume C in G;
    then ex P being Subset of Y st C = P & P is closed & A c= P;
    hence thesis;
  end;
  then reconsider G as Subset-Family of Y;
A1: now
    let C be set;
    assume C in G;
    then ex F being Subset of Y st F = C & F is closed & A c= F;
    hence MaxADSet(A) c= C by Th40;
  end;
  assume {F where F is Subset of Y : F is closed & A c= F} <> {};
  hence thesis by A1,SETFAM_1:5;
end;

begin

:: 4. Anti-discrete and Maximal Anti-discrete Subsets of Topological Spaces.

definition
  let X be non empty TopSpace;
  let A be Subset of X;
  redefine attr A is anti-discrete means
  :Def12:
  for x being Point of X st x in A holds A c= Cl {x};
  compatibility
  proof
    thus A is anti-discrete implies for x being Point of X st x in A holds A
    c= Cl {x}
    proof
      assume
A1:   A is anti-discrete;
      let x be Point of X;
      assume
A2:   x in A;
      {x} c= Cl {x} by PRE_TOPC:18;
      then
A3:   x in Cl {x} by ZFMISC_1:31;
      A misses Cl {x} or A c= Cl {x} by A1,Def4;
      hence A c= Cl {x} by A2,A3,XBOOLE_0:3;
    end;
    thus (for x being Point of X st x in A holds A c= Cl {x}) implies A is
    anti-discrete
    proof
      assume
A4:   for x being Point of X st x in A holds A c= Cl {x};
      now
        let F be Subset of X;
        assume
A5:     F is closed;
        assume A meets F;
        then consider a being set such that
A6:     a in A /\ F by XBOOLE_0:4;
        reconsider a as Point of X by A6;
        a in F by A6,XBOOLE_0:def 4;
        then {a} c= F by ZFMISC_1:31;
        then
A7:     Cl {a} c= F by A5,TOPS_1:5;
        a in A by A6,XBOOLE_0:def 4;
        then A c= Cl {a} by A4;
        hence A c= F by A7,XBOOLE_1:1;
      end;
      hence thesis by Def4;
    end;
  end;
end;

definition
  let X be non empty TopSpace;
  let A be Subset of X;
  redefine attr A is anti-discrete means
  for x being Point of X st x in A holds Cl A = Cl {x};
  compatibility
  proof
    thus A is anti-discrete implies for x being Point of X st x in A holds Cl
    A = Cl {x}
    proof
      assume
A1:   A is anti-discrete;
      let x be Point of X;
      assume
A2:   x in A;
      then {x} c= A by ZFMISC_1:31;
      then
A3:   Cl {x} c= Cl A by PRE_TOPC:19;
      A c= Cl {x} by A1,A2,Def12;
      then Cl A c= Cl {x} by TOPS_1:5;
      hence thesis by A3,XBOOLE_0:def 10;
    end;
    assume
A4: for x being Point of X st x in A holds Cl A = Cl {x};
    now
      let x be Point of X;
      assume x in A;
      then Cl A = Cl {x} by A4;
      hence A c= Cl {x} by PRE_TOPC:18;
    end;
    hence thesis by Def12;
  end;
end;

definition
  let X be non empty TopSpace;
  let A be Subset of X;
  redefine attr A is anti-discrete means
  :Def14:
  for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y};
  compatibility
  proof
    thus A is anti-discrete implies for x, y being Point of X st x in A & y in
    A holds Cl {x} = Cl {y}
    proof
      assume
A1:   A is anti-discrete;
      let x, y be Point of X;
      assume that
A2:   x in A and
A3:   y in A;
      A c= Cl {y} by A1,A3,Def12;
      then {x} c= Cl {y} by A2,ZFMISC_1:31;
      then
A4:   Cl {x} c= Cl {y} by TOPS_1:5;
      A c= Cl {x} by A1,A2,Def12;
      then {y} c= Cl {x} by A3,ZFMISC_1:31;
      then Cl {y} c= Cl {x} by TOPS_1:5;
      hence thesis by A4,XBOOLE_0:def 10;
    end;
    thus (for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y})
    implies A is anti-discrete
    proof
      assume
A5:   for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y};
      now
        let x be Point of X;
        assume
A6:     x in A;
        now
          let a be set;
          assume
A7:       a in A;
          then reconsider y = a as Point of X;
          {y} c= Cl {y} by PRE_TOPC:18;
          then y in Cl {y} by ZFMISC_1:31;
          hence a in Cl {x} by A5,A6,A7;
        end;
        hence A c= Cl {x} by TARSKI:def 3;
      end;
      hence thesis by Def12;
    end;
  end;
end;

reserve X for non empty TopSpace;

theorem
  for x being Point of X, D being Subset of X st D is anti-discrete & Cl
  {x} c= D holds D = Cl {x}
proof
  let x be Point of X, D be Subset of X;
  assume D is anti-discrete;
  then D misses Cl {x} or D c= Cl {x} by Def4;
  then
A1: D /\ Cl {x} = {} or D c= Cl {x} by XBOOLE_0:def 7;
  assume Cl {x} c= D;
  hence thesis by A1,XBOOLE_0:def 10,XBOOLE_1:28;
end;

theorem
  for A being Subset of X holds A is anti-discrete & A is closed iff for
  x being Point of X st x in A holds A = Cl {x}
proof
  let A be Subset of X;
  thus A is anti-discrete & A is closed implies for x being Point of X st x in
  A holds A = Cl {x}
  proof
    assume
A1: A is anti-discrete;
    assume
A2: A is closed;
    let x be Point of X;
    assume
A3: x in A;
    then {x} c= A by ZFMISC_1:31;
    then
A4: Cl {x} c= A by A2,TOPS_1:5;
    A c= Cl {x} by A1,A3,Def12;
    hence thesis by A4,XBOOLE_0:def 10;
  end;
  thus (for x being Point of X st x in A holds A = Cl {x}) implies A is
  anti-discrete & A is closed
  proof
    assume
A5: for x being Point of X st x in A holds A = Cl {x};
    then for x be Point of X st x in A holds A c= Cl {x};
    hence A is anti-discrete by Def12;
    hereby
      per cases;
      suppose
        A is empty;
        hence thesis;
      end;
      suppose
        A is non empty;
        then consider a being set such that
A6:     a in A by XBOOLE_0:def 1;
        reconsider a as Point of X by A6;
        A = Cl {a} by A5,A6;
        hence thesis;
      end;
    end;
  end;
end;

theorem
  for A being Subset of X holds A is anti-discrete & A is not open
  implies A is boundary
proof
  let A be Subset of X;
A1: Int A c= A by TOPS_1:16;
  assume A is anti-discrete;
  then A misses Int A or A c= Int A by Def3;
  then
A2: A /\ Int A = {} or A c= Int A by XBOOLE_0:def 7;
  assume
A3: A is not open;
  assume A is not boundary;
  then Int A <> {} by TOPS_1:48;
  hence contradiction by A3,A2,A1,XBOOLE_0:def 10,XBOOLE_1:28;
end;

theorem Th45:
  for x being Point of X st Cl {x} = {x} holds {x} is maximal_anti-discrete
proof
  let x be Point of X;
  assume
A1: Cl {x} = {x};
  {x} is anti-discrete by Th6;
  hence thesis by A1,Th17;
end;

reserve x,y for Point of X;

theorem Th46:
  MaxADSet(x) c= meet {G where G is Subset of X : G is open & x in G}
proof
  set F = {G where G is Subset of X : G is open & x in G};
  F c= bool the carrier of X
  proof
    let C be set;
    assume C in F;
    then ex P being Subset of X st C = P & P is open & x in P;
    hence thesis;
  end;
  then reconsider F as Subset-Family of X;
  now
    let C be set;
    assume C in F;
    then ex G being Subset of X st G = C & G is open & x in G;
    hence MaxADSet(x) c= C by Th24;
  end;
  hence thesis by SETFAM_1:5;
end;

theorem Th47:
  MaxADSet(x) c= meet {F where F is Subset of X : F is closed & x in F}
proof
  set G = {F where F is Subset of X : F is closed & x in F};
  G c= bool the carrier of X
  proof
    let C be set;
    assume C in G;
    then ex P being Subset of X st C = P & P is closed & x in P;
    hence thesis;
  end;
  then reconsider G as Subset-Family of X;
  now
    let C be set;
    assume C in G;
    then ex F being Subset of X st F = C & F is closed & x in F;
    hence MaxADSet(x) c= C by Th23;
  end;
  hence thesis by SETFAM_1:5;
end;

theorem Th48:
  MaxADSet(x) c= Cl {x}
proof
  Cl {x} = meet {F where F is Subset of X : F is closed & x in F} by Th2;
  hence thesis by Th47;
end;

Lm1: MaxADSet(x) = MaxADSet(y) implies Cl {x} = Cl {y}
proof
  assume
A1: MaxADSet(x) = MaxADSet(y);
  then
A2: y in MaxADSet(x) by Th21;
  MaxADSet(y) is maximal_anti-discrete by Th20;
  then
A3: MaxADSet(y) is anti-discrete by Def7;
  x in MaxADSet(y) by A1,Th21;
  hence thesis by A1,A2,A3,Def14;
end;

theorem Th49:
  MaxADSet(x) = MaxADSet(y) iff Cl {x} = Cl {y}
proof
A1: MaxADSet(x) c= MaxADSet(x) \/ MaxADSet(y) by XBOOLE_1:7;
  thus MaxADSet(x) = MaxADSet(y) implies Cl {x} = Cl {y} by Lm1;
A2: MaxADSet(y) c= MaxADSet(x) \/ MaxADSet(y) by XBOOLE_1:7;
  assume
A3: Cl {x} = Cl {y};
  now
    let a be Point of X;
    assume
A4: a in MaxADSet(x) \/ MaxADSet(y);
    now
      per cases by A4,XBOOLE_0:def 3;
      suppose
        a in MaxADSet(x);
        then
A5:     MaxADSet(a) = MaxADSet(x) by Th21;
        then Cl {a} = Cl {x} by Lm1;
        then
A6:     MaxADSet(y) c= Cl {a} by A3,Th48;
        MaxADSet(x) c= Cl {a} by A5,Th48;
        hence MaxADSet(x) \/ MaxADSet(y) c= Cl {a} by A6,XBOOLE_1:8;
      end;
      suppose
        a in MaxADSet(y);
        then
A7:     MaxADSet(a) = MaxADSet(y) by Th21;
        then Cl {a} = Cl {y} by Lm1;
        then
A8:     MaxADSet(x) c= Cl {a} by A3,Th48;
        MaxADSet(y) c= Cl {a} by A7,Th48;
        hence MaxADSet(x) \/ MaxADSet(y) c= Cl {a} by A8,XBOOLE_1:8;
      end;
    end;
    hence MaxADSet(x) \/ MaxADSet(y) c= Cl {a};
  end;
  then
A9: MaxADSet(x) \/ MaxADSet(y) is anti-discrete by Def12;
A10: MaxADSet(y) is maximal_anti-discrete by Th20;
  MaxADSet(x) is maximal_anti-discrete by Th20;
  then MaxADSet(x) = MaxADSet(x) \/ MaxADSet(y) by A9,A1,Def7;
  hence thesis by A9,A10,A2,Def7;
end;

theorem
  MaxADSet(x) misses MaxADSet(y) iff Cl {x} <> Cl {y}
proof
  thus MaxADSet(x) misses MaxADSet(y) implies Cl {x} <> Cl {y} by Th49;
  assume
A1: Cl {x} <> Cl {y};
  assume MaxADSet(x) meets MaxADSet(y);
  then MaxADSet(x) = MaxADSet(y) by Th22;
  hence contradiction by A1,Th49;
end;

definition
  let X be non empty TopSpace, x be Point of X;
  redefine func MaxADSet(x) -> non empty Subset of X equals
  (Cl {x}) /\ meet {
  G where G is Subset of X : G is open & x in G};
  compatibility
  proof
    set F = {G where G is Subset of X : G is open & x in G};
    F c= bool the carrier of X
    proof
      let C be set;
      assume C in F;
      then ex P being Subset of X st C = P & P is open & x in P;
      hence thesis;
    end;
    then reconsider F as Subset-Family of X;
A1: MaxADSet(x) c= Cl {x} by Th48;
A2: (Cl {x}) /\ meet F c= MaxADSet(x)
    proof
      assume not (Cl {x}) /\ meet F c= MaxADSet(x);
      then ((Cl {x}) /\ meet F) \ MaxADSet(x) <> {} by XBOOLE_1:37;
      then consider a being set such that
A3:   a in ((Cl {x}) /\ meet F) \ MaxADSet(x) by XBOOLE_0:def 1;
A4:   a in (Cl {x}) /\ meet F by A3,XBOOLE_0:def 5;
      reconsider a as Point of X by A3;
      not a in MaxADSet(x) by A3,XBOOLE_0:def 5;
      then
A5:   MaxADSet(a) <> MaxADSet(x) by Th21;
      now
        set G = (Cl{a})`;
        {a} c= Cl {a} by PRE_TOPC:18;
        then
A6:     a in Cl {a} by ZFMISC_1:31;
        assume not x in Cl {a};
        then x in G by SUBSET_1:29;
        then G in F;
        then
A7:     meet F c= G by SETFAM_1:3;
        a in meet F by A4,XBOOLE_0:def 4;
        hence contradiction by A7,A6,XBOOLE_0:def 5;
      end;
      then {x} c= Cl {a} by ZFMISC_1:31;
      then
A8:   Cl {x} c= Cl {a} by TOPS_1:5;
      a in Cl {x} by A4,XBOOLE_0:def 4;
      then {a} c= Cl {x} by ZFMISC_1:31;
      then Cl {a} c= Cl {x} by TOPS_1:5;
      then Cl {x} = Cl {a} by A8,XBOOLE_0:def 10;
      hence contradiction by A5,Th49;
    end;
    MaxADSet(x) c= meet F by Th46;
    then MaxADSet(x) c= (Cl {x}) /\ meet F by A1,XBOOLE_1:19;
    hence thesis by A2,XBOOLE_0:def 10;
  end;
  coherence;
end;

theorem Th51:
  for x, y being Point of X holds Cl {x} c= Cl {y} iff meet {G
where G is Subset of X : G is open & y in G} c= meet {G where G is Subset of X
  : G is open & x in G}
proof
  let x, y be Point of X;
  set FX = {G where G is Subset of X : G is open & x in G};
  set FY = {G where G is Subset of X : G is open & y in G};
A1: [#]X in FX;
  thus Cl {x} c= Cl {y} implies meet {G where G is Subset of X : G is open & y
  in G} c= meet {G where G is Subset of X : G is open & x in G}
  proof
    assume
A2: Cl {x} c= Cl {y};
    now
      let P be set;
      assume P in FX;
      then consider G being Subset of X such that
A3:   G = P and
A4:   G is open and
A5:   x in G;
      now
        assume not y in G;
        then {y} misses G by ZFMISC_1:50;
        then
A6:     (Cl {y}) misses G by A4,TSEP_1:36;
        {x} c= Cl {x} by PRE_TOPC:18;
        then x in Cl {x} by ZFMISC_1:31;
        hence contradiction by A2,A5,A6,XBOOLE_0:3;
      end;
      hence P in FY by A3,A4;
    end;
    then FX c= FY by TARSKI:def 3;
    hence thesis by A1,SETFAM_1:6;
  end;
  assume
A7: meet {G where G is Subset of X : G is open & y in G} c= meet {G
  where G is Subset of X : G is open & x in G};
  set G = (Cl {y})`;
  assume
A8: not Cl {x} c= Cl {y};
  now
    assume x in Cl {y};
    then {x} c= Cl {y} by ZFMISC_1:31;
    hence contradiction by A8,TOPS_1:5;
  end;
  then x in G by SUBSET_1:29;
  then G in FX;
  then meet FX c= G by SETFAM_1:3;
  then
A9: meet FY c= G by A7,XBOOLE_1:1;
  {y} c= Cl {y} by PRE_TOPC:18;
  then
A10: y in Cl {y} by ZFMISC_1:31;
  {y} c= MaxADSet(y) by Th12;
  then
A11: y in MaxADSet(y) by ZFMISC_1:31;
  MaxADSet(y) c= meet FY by Th46;
  then y in meet FY by A11;
  hence contradiction by A9,A10,XBOOLE_0:def 5;
end;

theorem
  for x, y being Point of X holds Cl {x} c= Cl {y} iff MaxADSet(y) c=
  meet {G where G is Subset of X : G is open & x in G}
proof
  let x, y be Point of X;
  set FY = {G where G is Subset of X : G is open & y in G};
  FY c= bool the carrier of X
  proof
    let C be set;
    assume C in FY;
    then ex P being Subset of X st C = P & P is open & y in P;
    hence thesis;
  end;
  then reconsider FY as Subset-Family of X;
  set FX = {G where G is Subset of X : G is open & x in G};
  FX c= bool the carrier of X
  proof
    let C be set;
    assume C in FX;
    then ex P being Subset of X st C = P & P is open & x in P;
    hence thesis;
  end;
  then reconsider FX as Subset-Family of X;
  thus Cl {x} c= Cl {y} implies MaxADSet(y) c= meet {G where G is Subset of X
  : G is open & x in G}
  proof
    assume Cl {x} c= Cl {y};
    then
A1: meet FY c= meet FX by Th51;
    (Cl {y}) /\ meet FY c= meet FY by XBOOLE_1:17;
    hence thesis by A1,XBOOLE_1:1;
  end;
  {y} c= MaxADSet(y) by Th12;
  then
A2: y in MaxADSet(y) by ZFMISC_1:31;
  assume MaxADSet(y) c= meet {G where G is Subset of X : G is open & x in G};
  then
A3: y in meet FX by A2;
  set G = (Cl {y})`;
  assume
A4: not Cl {x} c= Cl {y};
  now
    assume x in Cl {y};
    then {x} c= Cl {y} by ZFMISC_1:31;
    hence contradiction by A4,TOPS_1:5;
  end;
  then x in G by SUBSET_1:29;
  then G in FX;
  then
A5: meet FX c= G by SETFAM_1:3;
  {y} c= Cl {y} by PRE_TOPC:18;
  then y in Cl {y} by ZFMISC_1:31;
  hence contradiction by A5,A3,XBOOLE_0:def 5;
end;

theorem Th53:
  for x, y being Point of X holds MaxADSet(x) misses MaxADSet(y)
iff (ex V being Subset of X st V is open & MaxADSet(x) c= V & V misses MaxADSet
(y)) or ex W being Subset of X st W is open & W misses MaxADSet(x) & MaxADSet(y
  ) c= W
proof
  let x, y be Point of X;
  thus MaxADSet(x) misses MaxADSet(y) implies (ex V being Subset of X st V is
open & MaxADSet(x) c= V & V misses MaxADSet(y)) or ex W being Subset of X st W
  is open & W misses MaxADSet(x) & MaxADSet(y) c= W
  proof
    set V = (Cl {y})`;
    set W = (Cl {x})`;
    assume
A1: MaxADSet(x) /\ MaxADSet(y) = {};
    assume
A2: for V being Subset of X holds V is open & MaxADSet(x) c= V implies
    V meets MaxADSet(y);
    now
      take W;
      thus W is open;
      MaxADSet(x) c= Cl {x} by Th48;
      hence W misses MaxADSet(x) by SUBSET_1:24;
      now
        MaxADSet(y) c= Cl {y} by Th48;
        then V misses MaxADSet(y) by SUBSET_1:24;
        then not MaxADSet(x) c= V by A2;
        then MaxADSet(x) \ V <> {} by XBOOLE_1:37;
        then consider b being set such that
A3:     b in MaxADSet(x) \ V by XBOOLE_0:def 1;
A4:     b in MaxADSet(x) by A3,XBOOLE_0:def 5;
        reconsider b as Point of X by A3;
        not b in V by A3,XBOOLE_0:def 5;
        then b in Cl {y} by SUBSET_1:29;
        then
A5:     {b} c= Cl {y} by ZFMISC_1:31;
        MaxADSet(b) = MaxADSet(x) by A4,Th21;
        then Cl {b} = Cl {x} by Th49;
        then
A6:     Cl {x} c= Cl {y} by A5,TOPS_1:5;
        assume not MaxADSet(y) c= W;
        then MaxADSet(y) \ W <> {} by XBOOLE_1:37;
        then consider a being set such that
A7:     a in MaxADSet(y) \ W by XBOOLE_0:def 1;
A8:     a in MaxADSet(y) by A7,XBOOLE_0:def 5;
        reconsider a as Point of X by A7;
        not a in W by A7,XBOOLE_0:def 5;
        then a in Cl {x} by SUBSET_1:29;
        then
A9:     {a} c= Cl {x} by ZFMISC_1:31;
        MaxADSet(a) = MaxADSet(y) by A8,Th21;
        then Cl {a} = Cl {y} by Th49;
        then Cl {y} c= Cl {x} by A9,TOPS_1:5;
        then Cl {x} = Cl {y} by A6,XBOOLE_0:def 10;
        then MaxADSet(x) = MaxADSet(y) by Th49;
        hence contradiction by A1;
      end;
      hence MaxADSet(y) c= W;
    end;
    hence thesis;
  end;
  assume
A10: (ex V being Subset of X st V is open & MaxADSet(x) c= V & V misses
  MaxADSet(y)) or ex W being Subset of X st W is open & W misses MaxADSet(x) &
  MaxADSet(y) c= W;
  assume MaxADSet(x) meets MaxADSet(y);
  then
A11: MaxADSet(x) = MaxADSet(y) by Th22;
  now
    per cases by A10;
    suppose
      ex V being Subset of X st V is open & MaxADSet(x) c= V & V
      misses MaxADSet(y);
      then consider V being Subset of X such that
      V is open and
A12:  MaxADSet(x) c= V and
A13:  V misses MaxADSet(y);
      V /\ MaxADSet(y) = {} by A13,XBOOLE_0:def 7;
      hence contradiction by A11,A12,XBOOLE_1:28;
    end;
    suppose
      ex W being Subset of X st W is open & W misses MaxADSet(x) &
      MaxADSet(y) c= W;
      then consider W being Subset of X such that
      W is open and
A14:  W misses MaxADSet(x) and
A15:  MaxADSet(y) c= W;
      W /\ MaxADSet(x) = {} by A14,XBOOLE_0:def 7;
      hence contradiction by A11,A15,XBOOLE_1:28;
    end;
  end;
  hence contradiction;
end;

theorem
  for x, y being Point of X holds MaxADSet(x) misses MaxADSet(y) iff (ex
  E being Subset of X st E is closed & MaxADSet(x) c= E & E misses MaxADSet(y))
  or ex F being Subset of X st F is closed & F misses MaxADSet(x) & MaxADSet(y)
  c= F
proof
  let x, y be Point of X;
  thus MaxADSet(x) misses MaxADSet(y) implies (ex E being Subset of X st E is
closed & MaxADSet(x) c= E & E misses MaxADSet(y)) or ex F being Subset of X st
  F is closed & F misses MaxADSet(x) & MaxADSet(y) c= F
  proof
    assume
A1: MaxADSet(x) misses MaxADSet(y);
    hereby
      per cases by A1,Th53;
      suppose
        ex V being Subset of X st V is open & MaxADSet(x) c= V & V
        misses MaxADSet(y);
        then consider V being Subset of X such that
A2:     V is open and
A3:     MaxADSet(x) c= V and
A4:     V misses MaxADSet(y);
        now
          take F = V`;
          thus F is closed by A2;
          thus F misses MaxADSet(x) by A3,SUBSET_1:24;
          thus MaxADSet(y) c= F by A4,SUBSET_1:23;
        end;
        hence thesis;
      end;
      suppose
        ex W being Subset of X st W is open & W misses MaxADSet(x) &
        MaxADSet(y) c= W;
        then consider W being Subset of X such that
A5:     W is open and
A6:     W misses MaxADSet(x) and
A7:     MaxADSet(y) c= W;
        now
          take E = W`;
          thus E is closed by A5;
          thus MaxADSet(x) c= E by A6,SUBSET_1:23;
          thus E misses MaxADSet(y) by A7,SUBSET_1:24;
        end;
        hence thesis;
      end;
    end;
  end;
  assume
A8: (ex E being Subset of X st E is closed & MaxADSet(x) c= E & E
  misses MaxADSet(y)) or ex F being Subset of X st F is closed & F misses
  MaxADSet(x) & MaxADSet(y) c= F;
  assume MaxADSet(x) meets MaxADSet(y);
  then
A9: MaxADSet(x) = MaxADSet(y) by Th22;
  now
    per cases by A8;
    suppose
      ex E being Subset of X st E is closed & MaxADSet(x) c= E & E
      misses MaxADSet(y);
      then consider E being Subset of X such that
      E is closed and
A10:  MaxADSet(x) c= E and
A11:  E misses MaxADSet(y);
      E /\ MaxADSet(y) = {} by A11,XBOOLE_0:def 7;
      hence contradiction by A9,A10,XBOOLE_1:28;
    end;
    suppose
      ex F being Subset of X st F is closed & F misses MaxADSet(x) &
      MaxADSet(y) c= F;
      then consider F being Subset of X such that
      F is closed and
A12:  F misses MaxADSet(x) and
A13:  MaxADSet(y) c= F;
      F /\ MaxADSet(x) = {} by A12,XBOOLE_0:def 7;
      hence contradiction by A9,A13,XBOOLE_1:28;
    end;
  end;
  hence contradiction;
end;

reserve A, B for Subset of X;
reserve P, Q for Subset of X;

theorem Th55:
  MaxADSet(A) c= meet {G where G is Subset of X : G is open & A c= G}
proof
  set F = {G where G is Subset of X : G is open & A c= G};
  F c= bool the carrier of X
  proof
    let C be set;
    assume C in F;
    then ex P being Subset of X st C = P & P is open & A c= P;
    hence thesis;
  end;
  then reconsider F as Subset-Family of X;
  [#]X in F;
  hence thesis by Th39;
end;

theorem Th56:
  P is open implies MaxADSet(P) = P
proof
  set F = {G where G is Subset of X : G is open & P c= G};
A1: P c= MaxADSet(P) by Th32;
  assume P is open;
  then P in F;
  then
A2: meet F c= P by SETFAM_1:3;
  MaxADSet(P) c= meet F by Th55;
  then MaxADSet(P) c= P by A2,XBOOLE_1:1;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem
  MaxADSet(Int A) = Int A by Th56;

theorem Th58:
  MaxADSet(A) c= meet {F where F is Subset of X : F is closed & A c= F}
proof
  set G = {F where F is Subset of X : F is closed & A c= F};
  G c= bool the carrier of X
  proof
    let C be set;
    assume C in G;
    then ex P being Subset of X st C = P & P is closed & A c= P;
    hence thesis;
  end;
  then reconsider G as Subset-Family of X;
  [#]X in G;
  hence thesis by Th41;
end;

theorem Th59:
  MaxADSet(A) c= Cl A
proof
  Cl A = meet {F where F is Subset of X : F is closed & A c= F} by Th1;
  hence thesis by Th58;
end;

theorem Th60:
  P is closed implies MaxADSet(P) = P
proof
  assume P is closed;
  then
A1: Cl P = P by PRE_TOPC:22;
A2: P c= MaxADSet(P) by Th32;
  MaxADSet(P) c= Cl P by Th59;
  hence thesis by A1,A2,XBOOLE_0:def 10;
end;

theorem
  MaxADSet(Cl A) = Cl A by Th60;

theorem
  Cl MaxADSet(A) = Cl A
proof
A1: Cl MaxADSet(A) c= Cl A by Th59,TOPS_1:5;
  Cl A c= Cl MaxADSet(A) by Th32,PRE_TOPC:19;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem
  MaxADSet(A) = MaxADSet(B) implies Cl A = Cl B
proof
A1: MaxADSet(A) c= Cl A by Th59;
A2: MaxADSet(B) c= Cl B by Th59;
  assume
A3: MaxADSet(A) = MaxADSet(B);
  then A c= MaxADSet(B) by Th32;
  then A c= Cl B by A2,XBOOLE_1:1;
  then
A4: Cl A c= Cl B by TOPS_1:5;
  B c= MaxADSet(A) by A3,Th32;
  then B c= Cl A by A1,XBOOLE_1:1;
  then Cl B c= Cl A by TOPS_1:5;
  hence thesis by A4,XBOOLE_0:def 10;
end;

theorem
  P is closed or Q is closed implies MaxADSet(P /\ Q) = MaxADSet(P) /\
  MaxADSet(Q)
proof
  assume
A1: P is closed or Q is closed;
A2: MaxADSet(P) /\ MaxADSet(Q) c= MaxADSet(P /\ Q)
  proof
    assume not MaxADSet(P) /\ MaxADSet(Q) c= MaxADSet(P /\ Q);
    then consider x being set such that
A3: x in MaxADSet(P) /\ MaxADSet(Q) and
A4: not x in MaxADSet(P /\ Q) by TARSKI:def 3;
    reconsider x as Point of X by A3;
    now
      per cases by A1;
      suppose
A5:     P is closed;
        then P = MaxADSet(P) by Th60;
        then x in P by A3,XBOOLE_0:def 4;
        then
A6:     MaxADSet(x) c= P by A5,Th23;
A7:     P /\ Q c= MaxADSet(P /\ Q) by Th32;
        x in MaxADSet(Q) by A3,XBOOLE_0:def 4;
        then consider D being set such that
A8:     x in D and
A9:     D in {MaxADSet(b) where b is Point of X : b in Q} by TARSKI:def 4;
        consider b being Point of X such that
A10:    D = MaxADSet(b) and
A11:    b in Q by A9;
        {b} c= MaxADSet(b) by Th12;
        then
A12:    b in MaxADSet(b) by ZFMISC_1:31;
        MaxADSet(x) = MaxADSet(b) by A8,A10,Th21;
        then b in P /\ Q by A6,A11,A12,XBOOLE_0:def 4;
        then MaxADSet(b) meets MaxADSet(P /\ Q) by A12,A7,XBOOLE_0:3;
        then MaxADSet(b) c= MaxADSet(P /\ Q) by Th30;
        hence contradiction by A4,A8,A10;
      end;
      suppose
A13:    Q is closed;
        then Q = MaxADSet(Q) by Th60;
        then x in Q by A3,XBOOLE_0:def 4;
        then
A14:    MaxADSet(x) c= Q by A13,Th23;
A15:    P /\ Q c= MaxADSet(P /\ Q) by Th32;
        x in MaxADSet(P) by A3,XBOOLE_0:def 4;
        then consider D being set such that
A16:    x in D and
A17:    D in {MaxADSet(b) where b is Point of X : b in P} by TARSKI:def 4;
        consider b being Point of X such that
A18:    D = MaxADSet(b) and
A19:    b in P by A17;
        {b} c= MaxADSet(b) by Th12;
        then
A20:    b in MaxADSet(b) by ZFMISC_1:31;
        MaxADSet(x) = MaxADSet(b) by A16,A18,Th21;
        then b in P /\ Q by A14,A19,A20,XBOOLE_0:def 4;
        then MaxADSet(b) meets MaxADSet(P /\ Q) by A20,A15,XBOOLE_0:3;
        then MaxADSet(b) c= MaxADSet(P /\ Q) by Th30;
        hence contradiction by A4,A16,A18;
      end;
    end;
    hence contradiction;
  end;
  MaxADSet(P /\ Q) c= MaxADSet(P) /\ MaxADSet(Q) by Th37;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem
  P is open or Q is open implies MaxADSet(P /\ Q) = MaxADSet(P) /\ MaxADSet(Q)
proof
  assume
A1: P is open or Q is open;
A2: MaxADSet(P) /\ MaxADSet(Q) c= MaxADSet(P /\ Q)
  proof
    assume not MaxADSet(P) /\ MaxADSet(Q) c= MaxADSet(P /\ Q);
    then consider x being set such that
A3: x in MaxADSet(P) /\ MaxADSet(Q) and
A4: not x in MaxADSet(P /\ Q) by TARSKI:def 3;
    reconsider x as Point of X by A3;
    now
      per cases by A1;
      suppose
A5:     P is open;
        then P = MaxADSet(P) by Th56;
        then x in P by A3,XBOOLE_0:def 4;
        then
A6:     MaxADSet(x) c= P by A5,Th24;
A7:     P /\ Q c= MaxADSet(P /\ Q) by Th32;
        x in MaxADSet(Q) by A3,XBOOLE_0:def 4;
        then consider D being set such that
A8:     x in D and
A9:     D in {MaxADSet(b) where b is Point of X : b in Q} by TARSKI:def 4;
        consider b being Point of X such that
A10:    D = MaxADSet(b) and
A11:    b in Q by A9;
        {b} c= MaxADSet(b) by Th12;
        then
A12:    b in MaxADSet(b) by ZFMISC_1:31;
        MaxADSet(x) = MaxADSet(b) by A8,A10,Th21;
        then b in P /\ Q by A6,A11,A12,XBOOLE_0:def 4;
        then MaxADSet(b) meets MaxADSet(P /\ Q) by A12,A7,XBOOLE_0:3;
        then MaxADSet(b) c= MaxADSet(P /\ Q) by Th30;
        hence contradiction by A4,A8,A10;
      end;
      suppose
A13:    Q is open;
        then Q = MaxADSet(Q) by Th56;
        then x in Q by A3,XBOOLE_0:def 4;
        then
A14:    MaxADSet(x) c= Q by A13,Th24;
A15:    P /\ Q c= MaxADSet(P /\ Q) by Th32;
        x in MaxADSet(P) by A3,XBOOLE_0:def 4;
        then consider D being set such that
A16:    x in D and
A17:    D in {MaxADSet(b) where b is Point of X : b in P} by TARSKI:def 4;
        consider b being Point of X such that
A18:    D = MaxADSet(b) and
A19:    b in P by A17;
        {b} c= MaxADSet(b) by Th12;
        then
A20:    b in MaxADSet(b) by ZFMISC_1:31;
        MaxADSet(x) = MaxADSet(b) by A16,A18,Th21;
        then b in P /\ Q by A14,A19,A20,XBOOLE_0:def 4;
        then MaxADSet(b) meets MaxADSet(P /\ Q) by A20,A15,XBOOLE_0:3;
        then MaxADSet(b) c= MaxADSet(P /\ Q) by Th30;
        hence contradiction by A4,A16,A18;
      end;
    end;
    hence contradiction;
  end;
  MaxADSet(P /\ Q) c= MaxADSet(P) /\ MaxADSet(Q) by Th37;
  hence thesis by A2,XBOOLE_0:def 10;
end;

begin

:: 5. Maximal Anti-discrete Subspaces.

reserve Y for non empty TopStruct;

theorem Th66:
  for Y0 being SubSpace of Y, A being Subset of Y st A = the
  carrier of Y0 holds Y0 is anti-discrete implies A is anti-discrete
proof
  let Y0 be SubSpace of Y, A be Subset of Y;
  assume
A1: A = the carrier of Y0;
  assume Y0 is anti-discrete;
  then
A2: the topology of Y0 = {{}, the carrier of Y0} by TDLAT_3:def 2;
  now
    let G be Subset of Y;
    reconsider H = A /\ G as Subset of Y0 by A1,XBOOLE_1:17;
    assume
A3: G is open;
    now
      take G;
      thus G in the topology of Y by A3,PRE_TOPC:def 2;
      thus H = G /\ [#]Y0 by A1;
    end;
    then H in the topology of Y0 by PRE_TOPC:def 4;
    then A /\ G = {} or A /\ G = the carrier of Y0 by A2,TARSKI:def 2;
    hence A misses G or A c= G by A1,XBOOLE_0:def 7,XBOOLE_1:17;
  end;
  hence thesis by Def3;
end;

theorem Th67:
  for Y0 being SubSpace of Y st Y0 is TopSpace-like for A being
  Subset of Y st A = the carrier of Y0 holds A is anti-discrete implies Y0 is
  anti-discrete
proof
  let Y0 be SubSpace of Y;
  assume
A1: Y0 is TopSpace-like;
  then
A2: the carrier of Y0 in the topology of Y0 by PRE_TOPC:def 1;
  let A be Subset of Y;
  assume
A3: A = the carrier of Y0;
  assume
A4: A is anti-discrete;
  now
    let D be set;
    assume
A5: D in the topology of Y0;
    then reconsider C = D as Subset of Y0;
    consider E being Subset of Y such that
A6: E in the topology of Y and
A7: C = E /\ [#]Y0 by A5,PRE_TOPC:def 4;
    reconsider E as Subset of Y;
A8: E is open by A6,PRE_TOPC:def 2;
    now
      per cases by A4,A8,Def3;
      suppose
        A misses E;
        hence C = {} or C = A by A3,A7,XBOOLE_0:def 7;
      end;
      suppose
        A c= E;
        hence C = {} or C = A by A3,A7,XBOOLE_1:28;
      end;
    end;
    hence D in {{},the carrier of Y0} by A3,TARSKI:def 2;
  end;
  then
A9: the topology of Y0 c= {{},the carrier of Y0} by TARSKI:def 3;
  {} in the topology of Y0 by A1,PRE_TOPC:1;
  then {{},the carrier of Y0} c= the topology of Y0 by A2,ZFMISC_1:32;
  then the topology of Y0 = {{},the carrier of Y0} by A9,XBOOLE_0:def 10;
  hence thesis by TDLAT_3:def 2;
end;

reserve X for non empty TopSpace,
  Y0 for non empty SubSpace of X;

theorem
  (for X0 being open SubSpace of X holds Y0 misses X0 or Y0 is SubSpace
  of X0) implies Y0 is anti-discrete
proof
  reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
  assume
A1: for X0 being open SubSpace of X holds Y0 misses X0 or Y0 is SubSpace of X0;
  now
    let G be Subset of X;
    assume
A2: G is open;
    now
      per cases;
      suppose
        G is empty;
        hence A misses G or A c= G by XBOOLE_1:65;
      end;
      suppose
        G is non empty;
        then consider X0 being strict open non empty SubSpace of X such that
A3:     G = the carrier of X0 by A2,TSEP_1:20;
        Y0 misses X0 or Y0 is SubSpace of X0 by A1;
        hence A misses G or A c= G by A3,TSEP_1:4,def 3;
      end;
    end;
    hence A misses G or A c= G;
  end;
  then A is anti-discrete by Def3;
  hence thesis by Th67;
end;

theorem
  (for X0 being closed SubSpace of X holds Y0 misses X0 or Y0 is
  SubSpace of X0) implies Y0 is anti-discrete
proof
  reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
  assume
A1: for X0 being closed SubSpace of X holds Y0 misses X0 or Y0 is
  SubSpace of X0;
  now
    let G be Subset of X;
    assume
A2: G is closed;
    now
      per cases;
      suppose
        G is empty;
        hence A misses G or A c= G by XBOOLE_1:65;
      end;
      suppose
        G is non empty;
        then consider X0 being strict closed non empty SubSpace of X such that
A3:     G = the carrier of X0 by A2,TSEP_1:15;
        Y0 misses X0 or Y0 is SubSpace of X0 by A1;
        hence A misses G or A c= G by A3,TSEP_1:4,def 3;
      end;
    end;
    hence A misses G or A c= G;
  end;
  then A is anti-discrete by Def4;
  hence thesis by Th67;
end;

theorem
  for Y0 being anti-discrete SubSpace of X for X0 being open SubSpace of
  X holds Y0 misses X0 or Y0 is SubSpace of X0
proof
  let Y0 be anti-discrete SubSpace of X;
  reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
  let X0 be open SubSpace of X;
  reconsider G = the carrier of X0 as Subset of X by TSEP_1:1;
A1: G is open by TSEP_1:16;
  A is anti-discrete by Th66;
  then A misses G or A c= G by A1,Def3;
  hence thesis by TSEP_1:4,def 3;
end;

theorem
  for Y0 being anti-discrete SubSpace of X for X0 being closed SubSpace
  of X holds Y0 misses X0 or Y0 is SubSpace of X0
proof
  let Y0 be anti-discrete SubSpace of X;
  reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
  let X0 be closed SubSpace of X;
  reconsider G = the carrier of X0 as Subset of X by TSEP_1:1;
A1: G is closed by TSEP_1:11;
  A is anti-discrete by Th66;
  then A misses G or A c= G by A1,Def4;
  hence thesis by TSEP_1:4,def 3;
end;

definition
  let Y be non empty TopStruct;
  let IT be SubSpace of Y;
  attr IT is maximal_anti-discrete means
  :Def16:
  IT is anti-discrete & for Y0
  being SubSpace of Y st Y0 is anti-discrete holds the carrier of IT c= the
  carrier of Y0 implies the carrier of IT = the carrier of Y0;
end;

registration
  let Y be non empty TopStruct;
  cluster maximal_anti-discrete -> anti-discrete for SubSpace of Y;
  coherence by Def16;
  cluster non anti-discrete -> non maximal_anti-discrete for SubSpace of Y;
  coherence;
end;

theorem Th72:
  for Y0 being non empty SubSpace of X, A being Subset of X st A =
  the carrier of Y0 holds Y0 is maximal_anti-discrete iff A is
  maximal_anti-discrete
proof
  let Y0 be non empty SubSpace of X, A be Subset of X;
  assume
A1: A = the carrier of Y0;
  thus Y0 is maximal_anti-discrete implies A is maximal_anti-discrete
  proof
    assume
A2: Y0 is maximal_anti-discrete;
A3: now
      let D be Subset of X;
      assume
A4:   D is anti-discrete;
      assume
A5:   A c= D;
      then D <> {} by A1;
      then consider X0 being strict non empty SubSpace of X such that
A6:   D = the carrier of X0 by TSEP_1:10;
      X0 is anti-discrete by A4,A6,Th67;
      hence A = D by A1,A2,A5,A6,Def16;
    end;
    A is anti-discrete by A1,A2,Th66;
    hence thesis by A3,Def7;
  end;
  assume
A7: A is maximal_anti-discrete;
A8: now
    let X0 be SubSpace of X;
    reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
    assume X0 is anti-discrete;
    then
A9: D is anti-discrete by Th66;
    assume the carrier of Y0 c= the carrier of X0;
    hence the carrier of Y0 = the carrier of X0 by A1,A7,A9,Def7;
  end;
  A is anti-discrete by A7,Def7;
  then Y0 is anti-discrete by A1,Th67;
  hence thesis by A8,Def16;
end;

registration
  let X be non empty TopSpace;
  cluster open anti-discrete -> maximal_anti-discrete for
non empty SubSpace of X
    ;
  coherence
  proof
    let X0 be non empty SubSpace of X;
    reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
    assume X0 is open;
    then
A1: A is open by TSEP_1:16;
    assume X0 is anti-discrete;
    then A is anti-discrete by Th66;
    then A is maximal_anti-discrete by A1,Th16;
    hence thesis by Th72;
  end;
  cluster open non maximal_anti-discrete -> non anti-discrete for non empty
    SubSpace of X;
  coherence;
  cluster anti-discrete non maximal_anti-discrete -> non open for non empty
    SubSpace of X;
  coherence;
  cluster closed anti-discrete -> maximal_anti-discrete for
non empty SubSpace of
    X;
  coherence
  proof
    let X0 be non empty SubSpace of X;
    reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
    assume X0 is closed;
    then
A2: A is closed by TSEP_1:11;
    assume X0 is anti-discrete;
    then A is anti-discrete by Th66;
    then A is maximal_anti-discrete by A2,Th17;
    hence thesis by Th72;
  end;
  cluster closed non maximal_anti-discrete -> non anti-discrete for non empty
    SubSpace of X;
  coherence;
  cluster anti-discrete non maximal_anti-discrete -> non closed for non empty
    SubSpace of X;
  coherence;
end;

definition
  let Y be TopStruct, x be Point of Y;
  func MaxADSspace(x) -> strict SubSpace of Y means
  :Def17:
  the carrier of it = MaxADSet(x);
  existence
  proof
    set D = MaxADSet(x);
    set Y0 = Y|D;
    take Y0;
    D = [#]Y0 by PRE_TOPC:def 5;
    hence thesis;
  end;
  uniqueness
  proof
    let Y1, Y2 be strict SubSpace of Y;
    assume that
A1: the carrier of Y1 = MaxADSet(x) and
A2: the carrier of Y2 = MaxADSet(x);
    set A1 = the carrier of Y1, A2 = the carrier of Y2;
A3: A2 = [#]Y2;
A4: A1 = [#]Y1;
    then A1 c= [#]Y by PRE_TOPC:def 4;
    then reconsider A1 as Subset of Y;
    Y1 = Y|A1 by A4,PRE_TOPC:def 5;
    hence thesis by A1,A2,A3,PRE_TOPC:def 5;
  end;
end;

registration
  let Y be non empty TopStruct, x be Point of Y;
  cluster MaxADSspace(x) -> non empty;
  coherence
  proof
    the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
    hence the carrier of MaxADSspace(x) is non empty;
  end;
end;

Lm2: for X1, X2 being SubSpace of Y holds the carrier of X1 c= the carrier of
X2 implies X1 is SubSpace of X2
proof
  let X1, X2 be SubSpace of Y;
  set A1 = the carrier of X1, A2 = the carrier of X2;
A1: A1 = [#]X1;
  assume
A2: A1 c= A2;
A3: A2 = [#]X2;
  for P being Subset of X1 holds P in the topology of X1 iff ex Q being
  Subset of X2 st Q in the topology of X2 & P = Q /\ A1
  proof
    let P be Subset of X1;
    thus P in the topology of X1 implies ex Q being Subset of X2 st Q in the
    topology of X2 & P = Q /\ A1
    proof
      assume P in the topology of X1;
      then consider R being Subset of Y such that
A4:   R in the topology of Y and
A5:   P = R /\ A1 by A1,PRE_TOPC:def 4;
      reconsider Q = R /\ A2 as Subset of X2 by XBOOLE_1:17;
      take Q;
      thus Q in the topology of X2 by A3,A4,PRE_TOPC:def 4;
      Q /\ A1 = R /\ (A2 /\ A1) by XBOOLE_1:16
        .= R /\ A1 by A2,XBOOLE_1:28;
      hence thesis by A5;
    end;
    given Q being Subset of X2 such that
A6: Q in the topology of X2 and
A7: P = Q /\ A1;
    consider R being Subset of Y such that
A8: R in the topology of Y and
A9: Q = R /\ [#]X2 by A6,PRE_TOPC:def 4;
    P = R /\ (A2 /\ A1) by A7,A9,XBOOLE_1:16
      .= R /\ A1 by A2,XBOOLE_1:28;
    hence thesis by A1,A8,PRE_TOPC:def 4;
  end;
  hence thesis by A1,A3,A2,PRE_TOPC:def 4;
end;

theorem
  for x being Point of Y holds Sspace(x) is SubSpace of MaxADSspace(x)
proof
  let x be Point of Y;
A1: the carrier of Sspace(x) = {x} by TEX_2:def 2;
  the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
  hence thesis by A1,Lm2,Th12;
end;

theorem
  for x, y being Point of Y holds y is Point of MaxADSspace(x) iff the
  TopStruct of MaxADSspace(y) = the TopStruct of MaxADSspace(x)
proof
  let x, y be Point of Y;
A1: the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
  thus y is Point of MaxADSspace(x) implies the TopStruct of MaxADSspace(y) =
  the TopStruct of MaxADSspace(x)
  proof
    assume y is Point of MaxADSspace(x);
    then MaxADSet(y) = MaxADSet(x) by A1,Th21;
    hence thesis by A1,Def17;
  end;
  assume
A2: the TopStruct of MaxADSspace(y) = the TopStruct of MaxADSspace(x);
  the carrier of MaxADSspace(y) = MaxADSet(y) by Def17;
  hence thesis by A2,Th21;
end;

theorem
  for x, y being Point of Y holds the carrier of MaxADSspace(x) misses
  the carrier of MaxADSspace(y) or the TopStruct of MaxADSspace(x) = the
  TopStruct of MaxADSspace(y)
proof
  let x, y be Point of Y;
  assume
A1: the carrier of MaxADSspace(x) meets the carrier of MaxADSspace(y);
A2: the carrier of MaxADSspace(y) = MaxADSet(y) by Def17;
  the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
  hence thesis by A2,A1,Th22,TSEP_1:5;
end;

registration
  let X be non empty TopSpace;
  cluster maximal_anti-discrete strict for SubSpace of X;
  existence
  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;
    consider X0 being strict non empty SubSpace of X such that
A2: MaxADSet(a) = the carrier of X0 by TSEP_1:10;
    take X0;
    MaxADSet(a) is maximal_anti-discrete by Th20;
    hence thesis by A2,Th72;
  end;
end;

registration
  let X be non empty TopSpace, x be Point of X;
  cluster MaxADSspace(x) -> maximal_anti-discrete;
  coherence
  proof
A1: MaxADSet(x) is maximal_anti-discrete by Th20;
    MaxADSet(x) = the carrier of MaxADSspace(x) by Def17;
    hence thesis by A1,Th72;
  end;
end;

theorem
  for X0 being closed non empty SubSpace of X, x being Point of X holds
  x is Point of X0 implies MaxADSspace(x) is SubSpace of X0
proof
  let X0 be closed non empty SubSpace of X, x be Point of X;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is closed by TSEP_1:11;
  assume x is Point of X0;
  then MaxADSet(x) c= A by A1,Th23;
  then the carrier of MaxADSspace(x) c= the carrier of X0 by Def17;
  hence thesis by Lm2;
end;

theorem
  for X0 being open non empty SubSpace of X, x being Point of X holds x
  is Point of X0 implies MaxADSspace(x) is SubSpace of X0
proof
  let X0 be open non empty SubSpace of X, x be Point of X;
  reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is open by TSEP_1:16;
  assume x is Point of X0;
  then MaxADSet(x) c= A by A1,Th24;
  then the carrier of MaxADSspace(x) c= the carrier of X0 by Def17;
  hence thesis by Lm2;
end;

theorem
  for x being Point of X st Cl {x} = {x} holds Sspace(x) is
  maximal_anti-discrete
proof
  let x be Point of X;
  assume Cl {x} = {x};
  then
A1: {x} is maximal_anti-discrete by Th45;
  the carrier of Sspace(x) = {x} by TEX_2:def 2;
  hence thesis by A1,Th72;
end;

notation
  let Y be TopStruct, A be Subset of Y;
  synonym Sspace(A) for Y|A;
end;

Lm3: for Y being TopStruct, A being Subset of Y holds the carrier of (Y|A) = A
proof
  let Y be TopStruct, A be Subset of Y;
  [#](Y|A) = A by PRE_TOPC:def 5;
  hence thesis;
end;

theorem
  for A being non empty Subset of Y holds A is Subset of Sspace(A)
proof
  let A be non empty Subset of Y;
  the carrier of Sspace(A) c= the carrier of Sspace(A);
  hence thesis by Lm3;
end;

theorem
  for Y0 being SubSpace of Y, A being non empty Subset of Y holds A is
  Subset of Y0 implies Sspace(A) is SubSpace of Y0
proof
  let Y0 be SubSpace of Y, A be non empty Subset of Y;
  assume A is Subset of Y0;
  then A c= the carrier of Y0;
  then the carrier of Sspace(A) c= the carrier of Y0 by Lm3;
  hence thesis by Lm2;
end;

registration
  let Y be non trivial TopStruct;
  cluster non proper strict for SubSpace of Y;
  existence
  proof
    [#]Y = the carrier of Y;
    then reconsider A0 = the carrier of Y as non empty Subset of Y;
    set Y0 = Y|A0;
    take Y0;
    A0 = [#]Y0 by PRE_TOPC:def 5;
    hence thesis by TEX_2:10;
  end;
end;

registration
  let Y be non trivial TopStruct, A be non trivial Subset
  of Y;
  cluster Sspace(A) -> non trivial;
  coherence by Lm3;
end;

registration
  let Y be non empty TopStruct, A be non proper Subset of Y;
  cluster Sspace(A) -> non proper;
  coherence
  proof
    now
      assume
A1:   Sspace(A) is proper;
      the carrier of Sspace(A) = A by Lm3;
      hence contradiction by A1,TEX_2:8;
    end;
    hence thesis;
  end;
end;

definition
  let Y be non empty TopStruct, A be Subset of Y;
  func MaxADSspace(A) -> strict SubSpace of Y means
  :Def18:
  the carrier of it = MaxADSet(A);
  existence
  proof
    set D = MaxADSet(A);
    set Y0 = Y|D;
    take Y0;
    D = [#]Y0 by PRE_TOPC:def 5;
    hence thesis;
  end;
  uniqueness
  proof
    let Y1, Y2 be strict SubSpace of Y;
    assume that
A1: the carrier of Y1 = MaxADSet(A) and
A2: the carrier of Y2 = MaxADSet(A);
    set A1 = the carrier of Y1, A2 = the carrier of Y2;
A3: A2 = [#]Y2;
A4: A1 = [#]Y1;
    then A1 c= [#]Y by PRE_TOPC:def 4;
    then reconsider A1 as Subset of Y;
    Y1 = Y|A1 by A4,PRE_TOPC:def 5;
    hence thesis by A1,A2,A3,PRE_TOPC:def 5;
  end;
end;

registration
  let Y be non empty TopStruct, A be non empty Subset of Y;
  cluster MaxADSspace(A) -> non empty;
  coherence
  proof
    the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
    hence the carrier of MaxADSspace(A) is non empty;
  end;
end;

theorem
  for A being non empty Subset of Y holds A is Subset of MaxADSspace(A)
proof
  let A be non empty Subset of Y;
  the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
  hence thesis by Th32;
end;

theorem
  for A being non empty Subset of Y holds Sspace(A) is SubSpace of
  MaxADSspace(A)
proof
  let A be non empty Subset of Y;
A1: the carrier of Sspace(A) = A by Lm3;
  the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
  hence thesis by A1,Lm2,Th32;
end;

theorem
  for x being Point of Y holds the TopStruct of MaxADSspace(x) = the
  TopStruct of MaxADSspace({x})
proof
  let x be Point of Y;
A1: the carrier of MaxADSspace({x}) = MaxADSet({x}) by Def18;
  the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
  hence thesis by A1,Th28,TSEP_1:5;
end;

theorem
  for A, B being non empty Subset of Y holds A c= B implies MaxADSspace(
  A) is SubSpace of MaxADSspace(B)
proof
  let A, B be non empty Subset of Y;
  assume
A1: A c= B;
A2: the carrier of MaxADSspace(B) = MaxADSet(B) by Def18;
  the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
  hence thesis by A2,A1,Lm2,Th31;
end;

theorem
  for A being non empty Subset of Y holds the TopStruct of MaxADSspace(A
  ) = the TopStruct of MaxADSspace(MaxADSet(A))
proof
  let A be non empty Subset of Y;
A1: the carrier of MaxADSspace(MaxADSet(A)) = MaxADSet(MaxADSet(A)) by Def18;
  the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
  hence thesis by A1,Th33,TSEP_1:5;
end;

theorem
  for A, B being non empty Subset of Y holds A is Subset of MaxADSspace(
  B) implies MaxADSspace(A) is SubSpace of MaxADSspace(B)
proof
  let A, B be non empty Subset of Y;
  assume
A1: A is Subset of MaxADSspace(B);
A2: the carrier of MaxADSspace(B) = MaxADSet(B) by Def18;
  the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
  hence thesis by A2,A1,Lm2,Th34;
end;

theorem
  for A, B being non empty Subset of Y holds B is Subset of MaxADSspace(
  A) & A is Subset of MaxADSspace(B) iff the TopStruct of MaxADSspace(A) = the
  TopStruct of MaxADSspace(B)
proof
  let A, B be non empty Subset of Y;
A1: the carrier of MaxADSspace(B) = MaxADSet(B) by Def18;
A2: the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
  hence B is Subset of MaxADSspace(A) & A is Subset of MaxADSspace(B) implies
  the TopStruct of MaxADSspace(A) = the TopStruct of MaxADSspace(B) by A1,Th35,
TSEP_1:5;
  assume the TopStruct of MaxADSspace(A) = the TopStruct of MaxADSspace(B);
  hence thesis by A2,A1,Th32;
end;

registration
  let Y be non trivial TopStruct, A be non trivial Subset of Y;
  cluster MaxADSspace(A) -> non trivial;
  coherence
  proof
     MaxADSet(A) is not trivial;
    hence thesis by Def18;
  end;
end;

registration
  let Y be non empty TopStruct, A be non proper Subset of Y;
  cluster MaxADSspace(A) -> non proper;
  coherence
  proof
    now
      assume
A1:   MaxADSspace(A) is proper;
      the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
      hence contradiction by A1,TEX_2:8;
    end;
    hence thesis;
  end;
end;

theorem
  for X0 being open SubSpace of X, A being non empty Subset of X holds A
  is Subset of X0 implies MaxADSspace(A) is SubSpace of X0
proof
  let X0 be open SubSpace of X, A be non empty Subset of X;
  reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
A1: D is open by TSEP_1:16;
  assume A is Subset of X0;
  then MaxADSet(A) c= D by A1,Th38;
  then the carrier of MaxADSspace(A) c= the carrier of X0 by Def18;
  hence thesis by Lm2;
end;

theorem
  for X0 being closed SubSpace of X, A being non empty Subset of X holds
  A is Subset of X0 implies MaxADSspace(A) is SubSpace of X0
proof
  let X0 be closed SubSpace of X, A be non empty Subset of X;
  reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
A1: D is closed by TSEP_1:11;
  assume A is Subset of X0;
  then MaxADSet(A) c= D by A1,Th40;
  then the carrier of MaxADSspace(A) c= the carrier of X0 by Def18;
  hence thesis by Lm2;
end;