tex_4.miz



    begin

    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 :: TEX_4:1

    

     Th1: for A be Subset of X holds ( Cl A) = ( meet { F where F be Subset of X : F is closed & A c= F })

    proof

      let A be Subset of X;

      set G = { F where F be Subset of X : F is closed & A c= F };

      

       A1: G c= ( bool the carrier of X)

      proof

        let C be object;

        assume C in G;

        then ex P be 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 be 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 be 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;

    end;

    theorem :: TEX_4:2

    

     Th2: for x be Point of X holds ( Cl {x}) = ( meet { F where F be Subset of X : F is closed & x in F })

    proof

      let x be Point of X;

      set G = { F where F be Subset of X : F is closed & x in F };

      set H = { F where F be Subset of X : F is closed & {x} c= F };

      now

        let P be object;

        assume P in G;

        then

        consider F be 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;

      now

        let P be object;

        assume P in H;

        then

        consider F be 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;

      ( 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);

          ( 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 :: TEX_4:3

    for A be Subset of X holds ( Int A) = ( union { G where G be Subset of X : G is open & G c= A })

    proof

      let A be Subset of X;

      set F = { G where G be Subset of X : G is open & G c= A };

      

       A1: F c= ( bool the carrier of X)

      proof

        let C be object;

        assume C in F;

        then ex P be Subset of X st C = P & P is open & P c= A;

        hence thesis;

      end;

       {} c= A;

      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 be 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 be 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;

    end;

    begin

    definition

      let Y be TopStruct;

      let IT be Subset of Y;

      :: TEX_4:def1

      attr IT is anti-discrete means for x be Point of Y, G be 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;

      :: original: anti-discrete

      redefine

      :: TEX_4:def2

      attr A is anti-discrete means for x be Point of Y, F be 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 be object 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;

          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;

        end;

        hereby

          assume

           A9: for x be Point of Y, F be 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 be object 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;

        end;

      end;

    end

    definition

      let Y be TopStruct;

      let A be Subset of Y;

      :: original: anti-discrete

      redefine

      :: TEX_4:def3

      attr A is anti-discrete means for G be 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 be object 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;

        end;

        assume

         A5: for G be Subset of Y st G is open holds A misses G or A c= G;

        for x be Point of Y, G be Subset of Y st G is open & x in G & x in A holds A c= G by A5, XBOOLE_0: 3;

        hence thesis;

      end;

    end

    definition

      let Y be TopStruct;

      let A be Subset of Y;

      :: original: anti-discrete

      redefine

      :: TEX_4:def4

      attr A is anti-discrete means for F be 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;

          assume A meets G;

          then A c= ((G ` ) ` ) by A2, SUBSET_1: 23;

          hence A c= G;

        end;

        hereby

          assume

           A3: for G be 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;

        end;

      end;

    end

    theorem :: TEX_4:4

    

     Th4: for Y0,Y1 be TopStruct, D0 be Subset of Y0, D1 be 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;

      end;

      hence thesis;

    end;

    reserve Y for non empty TopStruct;

    theorem :: TEX_4:5

    

     Th5: for A,B be 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) <> {} ;

        then (A /\ G) <> {} by A1, XBOOLE_1: 3, XBOOLE_1: 26;

        then A meets G;

        then A c= G by A2, A3;

        hence B c= G by A1;

      end;

      hence thesis;

    end;

    theorem :: TEX_4:6

    

     Th6: for x be 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 be object 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;

    end;

    theorem :: TEX_4:7

    for A be empty Subset of Y holds A is anti-discrete;

    definition

      let Y be TopStruct;

      let IT be Subset-Family of Y;

      :: TEX_4:def5

      attr IT is anti-discrete-set-family means for A be Subset of Y st A in IT holds A is anti-discrete;

    end

    theorem :: TEX_4:8

    

     Th8: for F be 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 be 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 be 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;

        then

         A6: A0 c= G by A3, A5;

        ( meet F) c= A0 by A4, SETFAM_1: 3;

        then

         A7: ( meet F) c= G by A6;

        for B be 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, XBOOLE_1: 19;

          then

           A9: B0 meets G;

          B0 is anti-discrete by A1, A8;

          hence thesis by A3, A9;

        end;

        hence thesis by ZFMISC_1: 76;

      end;

      hence thesis;

    end;

    theorem :: TEX_4:9

    for F be 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;

        end;

          suppose ( meet F) <> {} ;

          ( meet F) c= ( union F) by SETFAM_1: 2;

          hence thesis by A1, Th5, Th8;

        end;

      end;

    end;

    definition

      let Y be TopStruct, x be Point of Y;

      :: TEX_4:def6

      func MaxADSF (x) -> Subset-Family of Y equals { A where A be Subset of Y : A is anti-discrete & x in A };

      coherence

      proof

        set F = { A where A be Subset of Y : A is anti-discrete & x in A };

        F c= ( bool the carrier of Y)

        proof

          let C be object;

          assume C in F;

          then ex A be 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 be 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 :: TEX_4:10

    

     Th10: ( MaxADSF x) is anti-discrete-set-family

    proof

      now

        let A be Subset of Y;

        assume A in ( MaxADSF x);

        then ex C be Subset of Y st C = A & C is anti-discrete & x in C;

        hence A is anti-discrete;

      end;

      hence thesis;

    end;

    theorem :: TEX_4:11

    

     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 be 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;

    end;

    theorem :: TEX_4:12

    

     Th12: {x} c= ( union ( MaxADSF x))

    proof

       {x} = ( meet ( MaxADSF x)) by Th11;

      hence thesis by SETFAM_1: 2;

    end;

    theorem :: TEX_4:13

    

     Th13: ( union ( MaxADSF x)) is anti-discrete

    proof

       {x} = ( meet ( MaxADSF x)) by Th11;

      hence thesis by Th8, Th10;

    end;

    begin

    definition

      let Y be TopStruct;

      let IT be Subset of Y;

      :: TEX_4:def7

      attr IT is maximal_anti-discrete means IT is anti-discrete & for D be Subset of Y st D is anti-discrete & IT c= D holds IT = D;

    end

    theorem :: TEX_4:14

    for Y0,Y1 be TopStruct, D0 be Subset of Y0, D1 be 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;

      end;

      D0 is anti-discrete by A3;

      then D1 is anti-discrete by A1, A2, Th4;

      hence thesis by A4;

    end;

    reserve Y for non empty TopStruct;

    theorem :: TEX_4:15

    

     Th15: for A be empty Subset of Y holds not A is maximal_anti-discrete

    proof

      consider a be object 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;

      end;

      hence thesis;

    end;

    theorem :: TEX_4:16

    

     Th16: for A be 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 be 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;

        then

         A3: (D /\ A) = {} or D c= A;

        assume A c= D;

        hence thesis by A3, XBOOLE_1: 28;

      end;

      hence thesis by A1;

    end;

    theorem :: TEX_4:17

    

     Th17: for A be 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 be 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;

        then

         A3: (D /\ A) = {} or D c= A;

        assume A c= D;

        hence thesis by A3, XBOOLE_1: 28;

      end;

      hence thesis by A1;

    end;

    definition

      let Y be TopStruct, x be Point of Y;

      :: TEX_4:def8

      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 :: TEX_4:18

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

    theorem :: TEX_4:19

    

     Th19: for D be Subset of Y, x be 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 be Subset of Y : A is anti-discrete & x in A } by A1;

      hence thesis by ZFMISC_1: 74;

    end;

    theorem :: TEX_4:20

    

     Th20: for x be Point of Y holds ( MaxADSet x) is maximal_anti-discrete

    proof

      let x be Point of Y;

      

       A1: for D be 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;

        then x in D by ZFMISC_1: 31;

        then D c= ( MaxADSet x) by A2, Th19;

        hence thesis by A3;

      end;

      ( MaxADSet x) is anti-discrete by Th13;

      hence thesis by A1;

    end;

    theorem :: TEX_4:21

    

     Th21: for x,y be 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;

      

       A2: ( MaxADSet x) is maximal_anti-discrete by Th20;

      then

       A3: ( MaxADSet x) is anti-discrete;

      thus y in ( MaxADSet x) implies ( MaxADSet y) = ( MaxADSet x)

      proof

        assume y in ( MaxADSet x);

        then ( MaxADSet x) in { A where A be 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;

      end;

      assume

       A4: ( MaxADSet y) = ( MaxADSet x);

       {y} c= ( MaxADSet y) by Th12;

      hence thesis by A4, ZFMISC_1: 31;

    end;

    theorem :: TEX_4:22

    

     Th22: for x,y be 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 be object 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 :: TEX_4:23

    

     Th23: for F be Subset of Y, x be 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;

      hence thesis by A1, A2, A3;

    end;

    theorem :: TEX_4:24

    

     Th24: for G be Subset of Y, x be 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;

      hence thesis by A1, A2, A3;

    end;

    theorem :: TEX_4:25

    for Y be non empty TopSpace, x be Point of Y holds ( MaxADSet x) c= ( meet { F where F be Subset of Y : F is closed & x in F })

    proof

      let Y be non empty TopSpace;

      let x be Point of Y;

      set G = { F where F be Subset of Y : F is closed & x in F };

      ( [#] Y) in G;

      then

       A1: G <> {} ;

      G c= ( bool the carrier of Y)

      proof

        let C be object;

        assume C in G;

        then ex P be 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 be 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, A1;

    end;

    theorem :: TEX_4:26

    for Y be non empty TopSpace, x be Point of Y holds ( MaxADSet x) c= ( meet { G where G be Subset of Y : G is open & x in G })

    proof

      let Y be non empty TopSpace;

      let x be Point of Y;

      set F = { G where G be Subset of Y : G is open & x in G };

      ( [#] Y) in F;

      then

       A1: F <> {} ;

      F c= ( bool the carrier of Y)

      proof

        let C be object;

        assume C in F;

        then ex P be 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 be 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, A1;

    end;

    definition

      let Y be non empty TopStruct;

      let A be Subset of Y;

      :: original: maximal_anti-discrete

      redefine

      :: TEX_4:def9

      attr A is maximal_anti-discrete means ex x be Point of Y st x in A & A = ( MaxADSet x);

      compatibility

      proof

        thus A is maximal_anti-discrete implies ex x be 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 be object 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;

          A is anti-discrete by A1;

          then A c= ( MaxADSet x) by A2, Th19;

          hence thesis by A1, A3;

        end;

        assume ex x be Point of Y st x in A & A = ( MaxADSet x);

        hence thesis by Th20;

      end;

    end

    theorem :: TEX_4:27

    

     Th27: for A be Subset of Y, x be Point of Y st x in A holds A is maximal_anti-discrete implies A = ( MaxADSet x) by Th21;

    definition

      let Y be non empty TopStruct;

      let A be non empty Subset of Y;

      :: original: maximal_anti-discrete

      redefine

      :: TEX_4:def10

      attr A is maximal_anti-discrete means for x be Point of Y st x in A holds A = ( MaxADSet x);

      compatibility

      proof

        thus A is maximal_anti-discrete implies for x be Point of Y st x in A holds A = ( MaxADSet x) by Th27;

        consider a be object such that

         A1: a in A by XBOOLE_0:def 1;

        reconsider a as Point of Y by A1;

        assume

         A2: for x be 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;

      end;

    end

    definition

      let Y be non empty TopStruct, A be Subset of Y;

      :: TEX_4:def11

      func MaxADSet (A) -> Subset of Y equals ( union { ( MaxADSet a) where a be Point of Y : a in A });

      coherence

      proof

        set M = { ( MaxADSet a) where a be Point of Y : a in A };

        M c= ( bool the carrier of Y)

        proof

          let C be object;

          assume C in M;

          then ex a be 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 :: TEX_4:28

    

     Th28: for x be Point of Y holds ( MaxADSet x) = ( MaxADSet {x})

    proof

      let x be Point of Y;

      set M = { ( MaxADSet a) where a be Point of Y : a in {x} };

      now

        let P be set;

        assume P in M;

        then ex a be 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;

    end;

    theorem :: TEX_4:29

    

     Th29: for A be Subset of Y, x be 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 be Point of Y : a in A };

      assume (( MaxADSet x) /\ ( MaxADSet A)) <> {} ;

      then

      consider z be object 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 be 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 be 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 :: TEX_4:30

    

     Th30: for A be Subset of Y, x be 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 be Point of Y : b in A };

      assume ( MaxADSet x) meets ( MaxADSet A);

      then ( MaxADSet x) meets A by Th29;

      then

      consider z be object 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 be 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 object;

        assume C in E;

        then ex a be 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 :: TEX_4:31

    

     Th31: for A,B be 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 be Point of Y : a in A };

      set F = { ( MaxADSet b) where b be Point of Y : b in B };

      assume

       A1: A c= B;

      E c= F

      proof

        let C be object;

        assume C in E;

        then ex a be Point of Y st C = ( MaxADSet a) & a in A;

        hence thesis by A1;

      end;

      hence thesis by ZFMISC_1: 77;

    end;

    theorem :: TEX_4:32

    

     Th32: for A be Subset of Y holds A c= ( MaxADSet A)

    proof

      let A be Subset of Y;

      let x be object;

      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;

      hence x in ( MaxADSet A) by A3;

    end;

    theorem :: TEX_4:33

    

     Th33: for A be 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 object;

        assume x in ( MaxADSet ( MaxADSet A));

        then

        consider C be set such that

         A2: x in C and

         A3: C in { ( MaxADSet a) where a be Point of Y : a in ( MaxADSet A) } by TARSKI:def 4;

        consider a be Point of Y such that

         A4: C = ( MaxADSet a) and

         A5: a in ( MaxADSet A) by A3;

        consider D be set such that

         A6: a in D and

         A7: D in { ( MaxADSet b) where b be Point of Y : b in A } by A5, TARSKI:def 4;

        consider b be 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;

    end;

    theorem :: TEX_4:34

    

     Th34: for A,B be 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 :: TEX_4:35

    

     Th35: for A,B be Subset of Y st B c= ( MaxADSet A) & A c= ( MaxADSet B) holds ( MaxADSet A) = ( MaxADSet B) by Th34;

    theorem :: TEX_4:36

    for A,B be 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 object;

        assume x in ( MaxADSet (A \/ B));

        then

        consider C be set such that

         A2: x in C and

         A3: C in { ( MaxADSet a) where a be Point of Y : a in (A \/ B) } by TARSKI:def 4;

        consider a be 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 be 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 be 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;

    end;

    theorem :: TEX_4:37

    

     Th37: for A,B be 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 be object such that

           A1: x in ( MaxADSet A);

          reconsider a = x as Point of Y by A1;

          consider D be set such that a in D and

           A2: D in { ( MaxADSet b) where b be Point of Y : b in A } by A1, TARSKI:def 4;

          ex b be 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;

        hence thesis;

      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 :: TEX_4:38

    

     Th38: for G be Subset of Y, A be 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 object;

        assume

         A3: x in ( MaxADSet A);

        then

        reconsider a = x as Point of Y;

        consider D be set such that

         A4: a in D and

         A5: D in { ( MaxADSet b) where b be Point of Y : b in A } by A3, TARSKI:def 4;

        consider b be 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;

        hence thesis by ZFMISC_1: 31;

      end;

      hence thesis;

    end;

    theorem :: TEX_4:39

    

     Th39: for Y be non empty TopSpace, A be Subset of Y holds ( MaxADSet A) c= ( meet { G where G be Subset of Y : G is open & A c= G })

    proof

      let Y be non empty TopSpace;

      let A be Subset of Y;

      set F = { G where G be Subset of Y : G is open & A c= G };

      ( [#] Y) in F;

      then

       A1: F <> {} ;

      F c= ( bool the carrier of Y)

      proof

        let C be object;

        assume C in F;

        then ex P be Subset of Y st C = P & P is open & A c= P;

        hence thesis;

      end;

      then

      reconsider F as Subset-Family of Y;

      now

        let C be set;

        assume C in F;

        then ex G be Subset of Y st G = C & G is open & A c= G;

        hence ( MaxADSet A) c= C by Th38;

      end;

      hence thesis by A1, SETFAM_1: 5;

    end;

    theorem :: TEX_4:40

    

     Th40: for F be Subset of Y, A be 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 object;

        assume

         A3: x in ( MaxADSet A);

        then

        reconsider a = x as Point of Y;

        consider D be set such that

         A4: a in D and

         A5: D in { ( MaxADSet b) where b be Point of Y : b in A } by A3, TARSKI:def 4;

        consider b be 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;

        hence thesis by ZFMISC_1: 31;

      end;

      hence thesis;

    end;

    theorem :: TEX_4:41

    

     Th41: for Y be non empty TopSpace, A be Subset of Y holds ( MaxADSet A) c= ( meet { F where F be Subset of Y : F is closed & A c= F })

    proof

      let Y be non empty TopSpace;

      let A be Subset of Y;

      set G = { F where F be Subset of Y : F is closed & A c= F };

      G c= ( bool the carrier of Y)

      proof

        let C be object;

        assume C in G;

        then ex P be 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 be Subset of Y st F = C & F is closed & A c= F;

        hence ( MaxADSet A) c= C by Th40;

      end;

      ( [#] Y) in G;

      then G <> {} ;

      hence thesis by A1, SETFAM_1: 5;

    end;

    begin

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: anti-discrete

      redefine

      :: TEX_4:def12

      attr A is anti-discrete means for x be Point of X st x in A holds A c= ( Cl {x});

      compatibility

      proof

        thus A is anti-discrete implies for x be 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;

          hence A c= ( Cl {x}) by A2, A3, XBOOLE_0: 3;

        end;

        thus (for x be Point of X st x in A holds A c= ( Cl {x})) implies A is anti-discrete

        proof

          assume

           A4: for x be 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 be object 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;

          end;

          hence thesis;

        end;

      end;

    end

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: anti-discrete

      redefine

      :: TEX_4:def13

      attr A is anti-discrete means for x be Point of X st x in A holds ( Cl A) = ( Cl {x});

      compatibility

      proof

        thus A is anti-discrete implies for x be Point of X st x in A holds ( Cl A) = ( Cl {x}) by ZFMISC_1: 31, PRE_TOPC: 19, TOPS_1: 5;

        assume

         A1: for x be 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 A1;

          hence A c= ( Cl {x}) by PRE_TOPC: 18;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: anti-discrete

      redefine

      :: TEX_4:def14

      attr A is anti-discrete means for x,y be 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 be 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;

          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;

          then {y} c= ( Cl {x}) by A3, ZFMISC_1: 31;

          then ( Cl {y}) c= ( Cl {x}) by TOPS_1: 5;

          hence thesis by A4;

        end;

        thus (for x,y be 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 be 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 object;

              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});

          end;

          hence thesis;

        end;

      end;

    end

    reserve X for non empty TopSpace;

    theorem :: TEX_4:42

    for x be Point of X, D be 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});

      then

       A1: (D /\ ( Cl {x})) = {} or D c= ( Cl {x});

      assume ( Cl {x}) c= D;

      hence thesis by A1, XBOOLE_1: 28;

    end;

    theorem :: TEX_4:43

    for A be Subset of X holds A is anti-discrete & A is closed iff for x be 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 be Point of X st x in A holds A = ( Cl {x}) by ZFMISC_1: 31, TOPS_1: 5;

      thus (for x be Point of X st x in A holds A = ( Cl {x})) implies A is anti-discrete & A is closed

      proof

        assume

         A1: for x be 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;

        hereby

          per cases ;

            suppose A is empty;

            hence thesis;

          end;

            suppose A is non empty;

            then

            consider a be object such that

             A2: a in A;

            reconsider a as Point of X by A2;

            A = ( Cl {a}) by A1, A2;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: TEX_4:44

    for A be Subset of X holds A is anti-discrete & not A is 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);

      then

       A2: (A /\ ( Int A)) = {} or A c= ( Int A);

      assume

       A3: not A is open;

      assume not A is boundary;

      then ( Int A) <> {} by TOPS_1: 48;

      hence contradiction by A3, A2, A1, XBOOLE_0:def 10, XBOOLE_1: 28;

    end;

    theorem :: TEX_4:45

    

     Th45: for x be 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 :: TEX_4:46

    

     Th46: ( MaxADSet x) c= ( meet { G where G be Subset of X : G is open & x in G })

    proof

      set F = { G where G be Subset of X : G is open & x in G };

      ( [#] X) in F;

      then

       A1: F <> {} ;

      F c= ( bool the carrier of X)

      proof

        let C be object;

        assume C in F;

        then ex P be 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 be Subset of X st G = C & G is open & x in G;

        hence ( MaxADSet x) c= C by Th24;

      end;

      hence thesis by A1, SETFAM_1: 5;

    end;

    theorem :: TEX_4:47

    

     Th47: ( MaxADSet x) c= ( meet { F where F be Subset of X : F is closed & x in F })

    proof

      set G = { F where F be Subset of X : F is closed & x in F };

      ( [#] X) in G;

      then

       A1: G <> {} ;

      G c= ( bool the carrier of X)

      proof

        let C be object;

        assume C in G;

        then ex P be 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 be Subset of X st F = C & F is closed & x in F;

        hence ( MaxADSet x) c= C by Th23;

      end;

      hence thesis by A1, SETFAM_1: 5;

    end;

    theorem :: TEX_4:48

    

     Th48: ( MaxADSet x) c= ( Cl {x})

    proof

      ( Cl {x}) = ( meet { F where F be 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;

      x in ( MaxADSet y) by A1, Th21;

      hence thesis by A1, A2, A3;

    end;

    theorem :: TEX_4:49

    

     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;

      

       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;

      hence thesis by A9, A10, A2;

    end;

    theorem :: TEX_4:50

    ( MaxADSet x) misses ( MaxADSet y) iff ( Cl {x}) <> ( Cl {y}) by Th49, Th22;

    definition

      let X be non empty TopSpace, x be Point of X;

      :: original: MaxADSet

      redefine

      :: TEX_4:def15

      func MaxADSet (x) -> non empty Subset of X equals (( Cl {x}) /\ ( meet { G where G be Subset of X : G is open & x in G }));

      compatibility

      proof

        set F = { G where G be Subset of X : G is open & x in G };

        F c= ( bool the carrier of X)

        proof

          let C be object;

          assume C in F;

          then ex P be 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 be object 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;

          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;

      end;

      coherence ;

    end

    theorem :: TEX_4:51

    

     Th51: for x,y be Point of X holds ( Cl {x}) c= ( Cl {y}) iff ( meet { G where G be Subset of X : G is open & y in G }) c= ( meet { G where G be Subset of X : G is open & x in G })

    proof

      let x,y be Point of X;

      set FX = { G where G be Subset of X : G is open & x in G };

      set FY = { G where G be Subset of X : G is open & y in G };

      

       A1: ( [#] X) in FX;

      thus ( Cl {x}) c= ( Cl {y}) implies ( meet { G where G be Subset of X : G is open & y in G }) c= ( meet { G where G be Subset of X : G is open & x in G })

      proof

        assume

         A2: ( Cl {x}) c= ( Cl {y});

        now

          let P be object;

          assume P in FX;

          then

          consider G be 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;

        hence thesis by A1, SETFAM_1: 6;

      end;

      assume

       A7: ( meet { G where G be Subset of X : G is open & y in G }) c= ( meet { G where G be Subset of X : G is open & x in G });

      set G = (( Cl {y}) ` );

      assume

       A8: not ( Cl {x}) c= ( Cl {y});

       not x in ( Cl {y}) by A8, TOPS_1: 5, ZFMISC_1: 31;

      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;

       {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 :: TEX_4:52

    for x,y be Point of X holds ( Cl {x}) c= ( Cl {y}) iff ( MaxADSet y) c= ( meet { G where G be Subset of X : G is open & x in G })

    proof

      let x,y be Point of X;

      set FY = { G where G be Subset of X : G is open & y in G };

      FY c= ( bool the carrier of X)

      proof

        let C be object;

        assume C in FY;

        then ex P be 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 be Subset of X : G is open & x in G };

      FX c= ( bool the carrier of X)

      proof

        let C be object;

        assume C in FX;

        then ex P be 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 be 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;

      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 be 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});

       not x in ( Cl {y}) by A4, TOPS_1: 5, ZFMISC_1: 31;

      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 :: TEX_4:53

    

     Th53: for x,y be Point of X holds ( MaxADSet x) misses ( MaxADSet y) iff (ex V be Subset of X st V is open & ( MaxADSet x) c= V & V misses ( MaxADSet y)) or ex W be 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 be Subset of X st V is open & ( MaxADSet x) c= V & V misses ( MaxADSet y)) or ex W be 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 be 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 be object 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 be object 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;

            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 be Subset of X st V is open & ( MaxADSet x) c= V & V misses ( MaxADSet y)) or ex W be 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 be Subset of X st V is open & ( MaxADSet x) c= V & V misses ( MaxADSet y);

          then

          consider V be 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;

          hence contradiction by A11, A12, XBOOLE_1: 28;

        end;

          suppose ex W be Subset of X st W is open & W misses ( MaxADSet x) & ( MaxADSet y) c= W;

          then

          consider W be 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;

          hence contradiction by A11, A15, XBOOLE_1: 28;

        end;

      end;

      hence contradiction;

    end;

    theorem :: TEX_4:54

    for x,y be Point of X holds ( MaxADSet x) misses ( MaxADSet y) iff (ex E be Subset of X st E is closed & ( MaxADSet x) c= E & E misses ( MaxADSet y)) or ex F be 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 be Subset of X st E is closed & ( MaxADSet x) c= E & E misses ( MaxADSet y)) or ex F be 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 be Subset of X st V is open & ( MaxADSet x) c= V & V misses ( MaxADSet y);

            then

            consider V be 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 be Subset of X st W is open & W misses ( MaxADSet x) & ( MaxADSet y) c= W;

            then

            consider W be 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 be Subset of X st E is closed & ( MaxADSet x) c= E & E misses ( MaxADSet y)) or ex F be 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 be Subset of X st E is closed & ( MaxADSet x) c= E & E misses ( MaxADSet y);

          then

          consider E be 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;

          hence contradiction by A9, A10, XBOOLE_1: 28;

        end;

          suppose ex F be Subset of X st F is closed & F misses ( MaxADSet x) & ( MaxADSet y) c= F;

          then

          consider F be 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;

          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 :: TEX_4:55

    

     Th55: ( MaxADSet A) c= ( meet { G where G be Subset of X : G is open & A c= G }) by Th39;

    theorem :: TEX_4:56

    

     Th56: P is open implies ( MaxADSet P) = P

    proof

      set F = { G where G be 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;

      hence thesis by A1;

    end;

    theorem :: TEX_4:57

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

    theorem :: TEX_4:58

    

     Th58: ( MaxADSet A) c= ( meet { F where F be Subset of X : F is closed & A c= F }) by Th41;

    theorem :: TEX_4:59

    

     Th59: ( MaxADSet A) c= ( Cl A)

    proof

      ( Cl A) = ( meet { F where F be Subset of X : F is closed & A c= F }) by Th1;

      hence thesis by Th58;

    end;

    theorem :: TEX_4:60

    

     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;

    end;

    theorem :: TEX_4:61

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

    theorem :: TEX_4:62

    ( Cl ( MaxADSet A)) = ( Cl A) by Th59, TOPS_1: 5, Th32, PRE_TOPC: 19;

    theorem :: TEX_4:63

    ( 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;

      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;

      then ( Cl B) c= ( Cl A) by TOPS_1: 5;

      hence thesis by A4;

    end;

    theorem :: TEX_4:64

    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 be object such that

         A3: x in (( MaxADSet P) /\ ( MaxADSet Q)) and

         A4: not x in ( MaxADSet (P /\ Q));

        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 be set such that

             A8: x in D and

             A9: D in { ( MaxADSet b) where b be Point of X : b in Q } by TARSKI:def 4;

            consider b be 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 be set such that

             A16: x in D and

             A17: D in { ( MaxADSet b) where b be Point of X : b in P } by TARSKI:def 4;

            consider b be 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;

    end;

    theorem :: TEX_4:65

    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 be object such that

         A3: x in (( MaxADSet P) /\ ( MaxADSet Q)) and

         A4: not x in ( MaxADSet (P /\ Q));

        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 be set such that

             A8: x in D and

             A9: D in { ( MaxADSet b) where b be Point of X : b in Q } by TARSKI:def 4;

            consider b be 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 be set such that

             A16: x in D and

             A17: D in { ( MaxADSet b) where b be Point of X : b in P } by TARSKI:def 4;

            consider b be 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;

    end;

    begin

    reserve Y for non empty TopStruct;

    theorem :: TEX_4:66

    

     Th66: for Y0 be SubSpace of Y, A be 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;

        G in the topology of Y & H = (G /\ ( [#] Y0)) by A1, A3, PRE_TOPC:def 2;

        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_1: 17;

      end;

      hence thesis;

    end;

    theorem :: TEX_4:67

    

     Th67: for Y0 be SubSpace of Y st Y0 is TopSpace-like holds for A be 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 object;

        assume

         A5: D in the topology of Y0;

        then

        reconsider C = D as Subset of Y0;

        consider E be 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;

            suppose A misses E;

            hence C = {} or C = A by A3, A7;

          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};

       {} 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;

      hence thesis by TDLAT_3:def 2;

    end;

    reserve X for non empty TopSpace,

Y0 for non empty SubSpace of X;

    theorem :: TEX_4:68

    (for X0 be 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 be 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;

          end;

            suppose G is non empty;

            then

            consider X0 be 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, TSEP_1:def 3;

          end;

        end;

        hence A misses G or A c= G;

      end;

      then A is anti-discrete;

      hence thesis by Th67;

    end;

    theorem :: TEX_4:69

    (for X0 be 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 be 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;

          end;

            suppose G is non empty;

            then

            consider X0 be 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, TSEP_1:def 3;

          end;

        end;

        hence A misses G or A c= G;

      end;

      then A is anti-discrete;

      hence thesis by Th67;

    end;

    theorem :: TEX_4:70

    for Y0 be anti-discrete SubSpace of X holds for X0 be 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;

      hence thesis by TSEP_1: 4, TSEP_1:def 3;

    end;

    theorem :: TEX_4:71

    for Y0 be anti-discrete SubSpace of X holds for X0 be 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;

      hence thesis by TSEP_1: 4, TSEP_1:def 3;

    end;

    definition

      let Y be non empty TopStruct;

      let IT be SubSpace of Y;

      :: TEX_4:def16

      attr IT is maximal_anti-discrete means IT is anti-discrete & for Y0 be 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 ;

      cluster non anti-discrete -> non maximal_anti-discrete for SubSpace of Y;

      coherence ;

    end

    theorem :: TEX_4:72

    

     Th72: for Y0 be non empty SubSpace of X, A be 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 be 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;

        end;

        A is anti-discrete by A1, A2, Th66;

        hence thesis by A3;

      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;

      end;

      A is anti-discrete by A7;

      then Y0 is anti-discrete by A1, Th67;

      hence thesis by A8;

    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;

      :: TEX_4:def17

      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 be 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 be Subset of X1 holds P in the topology of X1 iff ex Q be 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 be Subset of X2 st Q in the topology of X2 & P = (Q /\ A1)

        proof

          assume P in the topology of X1;

          then

          consider R be 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 be Subset of X2 such that

         A6: Q in the topology of X2 and

         A7: P = (Q /\ A1);

        consider R be 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 :: TEX_4:73

    for x be 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 :: TEX_4:74

    for x,y be 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 :: TEX_4:75

    for x,y be 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 be object such that

         A1: a in the carrier of X by XBOOLE_0:def 1;

        reconsider a as Point of X by A1;

        consider X0 be 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 :: TEX_4:76

    for X0 be closed non empty SubSpace of X, x be 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 :: TEX_4:77

    for X0 be open non empty SubSpace of X, x be 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 :: TEX_4:78

    for x be 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 be TopStruct, A be 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 :: TEX_4:79

    for A be 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 :: TEX_4:80

    for Y0 be SubSpace of Y, A be 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;

      :: TEX_4:def18

      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 :: TEX_4:81

    for A be 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 :: TEX_4:82

    for A be 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 :: TEX_4:83

    for x be 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 :: TEX_4:84

    for A,B be 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 :: TEX_4:85

    for A be 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 :: TEX_4:86

    for A,B be 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 :: TEX_4:87

    for A,B be 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

         not ( MaxADSet A) is 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 :: TEX_4:88

    for X0 be open SubSpace of X, A be 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 :: TEX_4:89

    for X0 be closed SubSpace of X, A be 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;