tdlat_3.miz

    begin

    reserve X for TopSpace;

    reserve C for Subset of X;

    theorem :: TDLAT_3:1



     Th1: ( Cl C) = (( Int (C ` )) ` )

    proof



      thus ( Cl C) = ((( Cl ((C ` ) ` )) ` ) ` )

      .= (( Int (C ` )) ` ) by TOPS_1:def 1;

    end;

    theorem :: TDLAT_3:2



     Th2: ( Cl (C ` )) = (( Int C) ` )

    proof



      thus ( Cl (C ` )) = (( Int ((C ` ) ` )) ` ) by Th1

      .= (( Int C) ` );

    end;

    theorem :: TDLAT_3:3



     Th3: ( Int (C ` )) = (( Cl C) ` )

    proof



      thus ( Int (C ` )) = (( Cl ((C ` ) ` )) ` ) by TOPS_1:def 1

      .= (( Cl C) ` );

    end;

    reserve A,B for Subset of X;

    theorem :: TDLAT_3:4

    (A \/ B) = the carrier of X implies (A is closed implies (A \/ ( Int B)) = the carrier of X)

    proof

      assume (A \/ B) = the carrier of X;

      then ((A \/ B) ` ) = ( {} X) by XBOOLE_1: 37;

      then ((A ` ) /\ (B ` )) = {} by XBOOLE_1: 53;

      then

       A1: (A ` ) misses (B ` );

      assume A is closed;

      then (A ` ) misses ( Cl (B ` )) by A1, TSEP_1: 36;

      then ((A ` ) /\ ((( Cl (B ` )) ` ) ` )) = {} ;

      then ((A ` ) /\ (( Int B) ` )) = {} by TOPS_1:def 1;

      then ((A \/ ( Int B)) ` ) = ( {} X) by XBOOLE_1: 53;

      then (((A \/ ( Int B)) ` ) ` ) = ( [#] X);

      hence thesis;

    end;

    theorem :: TDLAT_3:5



     Th5: A is open closed iff ( Cl A) = ( Int A)

    proof

      thus A is open & A is closed implies ( Cl A) = ( Int A)

      proof

        assume that

         A1: A is open and

         A2: A is closed;

        ( Int A) = A by A1, TOPS_1: 23;

        hence thesis by A2, PRE_TOPC: 22;

      end;



       A3: ( Int A) c= A by TOPS_1: 16;



       A4: A c= ( Cl A) by PRE_TOPC: 18;

      assume ( Cl A) = ( Int A);

      hence thesis by A3, A4, XBOOLE_0:def 10;

    end;

    theorem :: TDLAT_3:6

    A is open & A is closed implies ( Int ( Cl A)) = ( Cl ( Int A))

    proof

      assume that

       A1: A is open and

       A2: A is closed;



       A3: ( Cl A) = A by A2, PRE_TOPC: 22;

      ( Int A) = A by A1, TOPS_1: 23;

      hence thesis by A3;

    end;

    theorem :: TDLAT_3:7



     Th7: A is condensed & ( Cl ( Int A)) c= ( Int ( Cl A)) implies A is open_condensed & A is closed_condensed

    proof

      assume

       A1: A is condensed;

      then

       A2: ( Int ( Cl A)) c= A by TOPS_1:def 6;



       A3: A c= ( Cl ( Int A)) by A1, TOPS_1:def 6;

      assume

       A4: ( Cl ( Int A)) c= ( Int ( Cl A));

      then ( Cl ( Int A)) c= A by A2;

      then

       A5: A = ( Cl ( Int A)) by A3;

      A c= ( Int ( Cl A)) by A3, A4;

      then A = ( Int ( Cl A)) by A2;

      hence thesis by A5, TOPS_1:def 7, TOPS_1:def 8;

    end;

    theorem :: TDLAT_3:8



     Th8: A is condensed & ( Cl ( Int A)) c= ( Int ( Cl A)) implies A is open & A is closed

    proof

      assume that

       A1: A is condensed and

       A2: ( Cl ( Int A)) c= ( Int ( Cl A));



       A3: A is closed_condensed by A1, A2, Th7;

      A is open_condensed by A1, A2, Th7;

      hence thesis by A3, TOPS_1: 66, TOPS_1: 67;

    end;

    theorem :: TDLAT_3:9



     Th9: A is condensed implies ( Int ( Cl A)) = ( Int A) & ( Cl A) = ( Cl ( Int A))

    proof



       A1: ( Cl ( Int A)) c= ( Cl A) by PRE_TOPC: 19, TOPS_1: 16;

      assume

       A2: A is condensed;

      then ( Int ( Cl A)) c= A by TOPS_1:def 6;

      then

       A3: ( Int ( Int ( Cl A))) c= ( Int A) by TOPS_1: 19;

      A c= ( Cl ( Int A)) by A2, TOPS_1:def 6;

      then

       A4: ( Cl A) c= ( Cl ( Cl ( Int A))) by PRE_TOPC: 19;

      ( Int A) c= ( Int ( Cl A)) by PRE_TOPC: 18, TOPS_1: 19;

      hence thesis by A3, A4, A1;

    end;

    begin

    definition

      let IT be TopStruct;

      :: TDLAT_3:def1

      attr IT is discrete means

      : Def1: the topology of IT = ( bool the carrier of IT);

      :: TDLAT_3:def2

      attr IT is anti-discrete means

      : Def2: the topology of IT = { {} , the carrier of IT};

    end

    theorem :: TDLAT_3:10

    for Y be TopStruct holds Y is discrete & Y is anti-discrete implies ( bool the carrier of Y) = { {} , the carrier of Y};

    theorem :: TDLAT_3:11



     Th11: for Y be TopStruct st {} in the topology of Y & the carrier of Y in the topology of Y holds ( bool the carrier of Y) = { {} , the carrier of Y} implies Y is discrete & Y is anti-discrete

    proof

      let Y be TopStruct;

      assume that

       A1: {} in the topology of Y and

       A2: the carrier of Y in the topology of Y;

      assume

       A3: ( bool the carrier of Y) = { {} , the carrier of Y};

       { {} , the carrier of Y} c= the topology of Y by A1, A2, ZFMISC_1: 32;

      then the topology of Y = ( bool the carrier of Y) by A3;

      hence thesis by A3;

    end;

    registration

      cluster discrete anti-discrete strict non empty for TopStruct;

      existence

      proof

        set one = { {} };

        reconsider tau = ( bool one) as Subset-Family of one;

        take Y = TopStruct (# one, tau #);

        thus Y is discrete;

        tau = { {} , one} by ZFMISC_1: 24;

        hence Y is anti-discrete;

        thus thesis;

      end;

    end

    theorem :: TDLAT_3:12

    for Y be discrete TopStruct, A be Subset of Y holds (the carrier of Y \ A) in the topology of Y

    proof

      let Y be discrete TopStruct, A be Subset of Y;

      the topology of Y = ( bool the carrier of Y) by Def1;

      hence thesis;

    end;

    theorem :: TDLAT_3:13



     Th13: for Y be anti-discrete TopStruct, A be Subset of Y st A in the topology of Y holds (the carrier of Y \ A) in the topology of Y

    proof

      let Y be anti-discrete TopStruct, A be Subset of Y;



       A1: the topology of Y = { {} , the carrier of Y} by Def2;

      assume A in the topology of Y;

      then A = {} or A = the carrier of Y by A1, TARSKI:def 2;

      then (the carrier of Y \ A) = the carrier of Y or (the carrier of Y \ A) = {} by XBOOLE_1: 37;

      hence thesis by A1, TARSKI:def 2;

    end;

    registration

      cluster discrete -> TopSpace-like for TopStruct;

      coherence

      proof

        let Y be TopStruct;

        assume Y is discrete;

        then

         A1: the topology of Y = ( bool the carrier of Y);

        then

         A2: for F be Subset-Family of Y st F c= the topology of Y holds ( union F) in the topology of Y;



         A3: for A,B be Subset of Y st A in the topology of Y & B in the topology of Y holds (A /\ B) in the topology of Y by A1;

        the carrier of Y in the topology of Y by A1, ZFMISC_1:def 1;

        hence thesis by A2, A3, PRE_TOPC:def 1;

      end;

      cluster anti-discrete -> TopSpace-like for TopStruct;

      coherence

      proof

        let Y be TopStruct;

        assume Y is anti-discrete;

        then

         A4: the topology of Y = { {} , the carrier of Y};



         A5: for A,B be Subset of Y st A in the topology of Y & B in the topology of Y holds (A /\ B) in the topology of Y

        proof

          let A,B be Subset of Y;

          assume that

           A6: A in the topology of Y and

           A7: B in the topology of Y;



           A8: B = {} or B = the carrier of Y by A4, A7, TARSKI:def 2;

          A = {} or A = the carrier of Y by A4, A6, TARSKI:def 2;

          hence thesis by A4, A8, TARSKI:def 2;

        end;



         A9: for F be Subset-Family of Y st F c= the topology of Y holds ( union F) in the topology of Y

        proof

          let F be Subset-Family of Y;

          assume F c= the topology of Y;

          then F = {} or F = { {} } or F = {the carrier of Y} or F = { {} , the carrier of Y} by A4, ZFMISC_1: 36;

          then ( union F) = {} or ( union F) = the carrier of Y or ( union F) = ( {} \/ the carrier of Y) by ZFMISC_1: 2, ZFMISC_1: 25, ZFMISC_1: 75;

          hence thesis by A4, TARSKI:def 2;

        end;

        the carrier of Y in the topology of Y by A4, TARSKI:def 2;

        hence thesis by A9, A5, PRE_TOPC:def 1;

      end;

    end

    theorem :: TDLAT_3:14

    for Y be TopSpace-like TopStruct holds ( bool the carrier of Y) = { {} , the carrier of Y} implies Y is discrete & Y is anti-discrete

    proof

      let Y be TopSpace-like TopStruct;

      reconsider E = {} as Subset-Family of Y by XBOOLE_1: 2;

      reconsider E as Subset-Family of Y;



       A1: the carrier of Y in the topology of Y by PRE_TOPC:def 1;

      E c= the topology of Y;

      then

       A2: {} in the topology of Y by PRE_TOPC:def 1, ZFMISC_1: 2;

      assume ( bool the carrier of Y) = { {} , the carrier of Y};

      hence thesis by A2, A1, Th11;

    end;

    definition

      let IT be TopStruct;

      :: TDLAT_3:def3

      attr IT is almost_discrete means for A be Subset of IT st A in the topology of IT holds (the carrier of IT \ A) in the topology of IT;

    end

    registration

      cluster discrete -> almost_discrete for TopStruct;

      coherence ;

      cluster anti-discrete -> almost_discrete for TopStruct;

      coherence by Th13;

    end

    registration

      cluster almost_discrete strict for TopStruct;

      existence

      proof

        set Y = the discrete strict TopStruct;

        take Y;

        thus thesis;

      end;

    end

    begin

    registration

      cluster discrete anti-discrete strict non empty for TopSpace;

      existence

      proof

        set X = the discrete anti-discrete strict non empty TopStruct;

        reconsider X as TopSpace;

        take X;

        thus thesis;

      end;

    end

    theorem :: TDLAT_3:15



     Th15: X is discrete iff for A be Subset of X holds A is open

    proof

      thus X is discrete implies for A be Subset of X holds A is open by PRE_TOPC:def 2;

      assume for A be Subset of X holds A is open;

      then for V be object holds V in the topology of X iff V in ( bool the carrier of X) by PRE_TOPC:def 2;

      then the topology of X = ( bool the carrier of X) by TARSKI: 2;

      hence thesis;

    end;

    theorem :: TDLAT_3:16



     Th16: X is discrete iff for A be Subset of X holds A is closed

    proof

      thus X is discrete implies for A be Subset of X holds A is closed

      proof

        assume

         A1: X is discrete;

        let A be Subset of X;

        (A ` ) is open by A1, Th15;

        hence thesis by TOPS_1: 3;

      end;

      assume

       A2: for A be Subset of X holds A is closed;

      now

        let A be Subset of X;

        (A ` ) is closed by A2;

        hence A is open by TOPS_1: 4;

      end;

      hence thesis by Th15;

    end;

    theorem :: TDLAT_3:17



     Th17: (for A be Subset of X, x be Point of X st A = {x} holds A is open) implies X is discrete

    proof

      assume

       A1: for A be Subset of X, x be Point of X st A = {x} holds A is open;

      now

        let A be Subset of X;

        set F = { B where B be Subset of X : ex a be Point of X st a in A & B = {a} };



         A2: F c= ( bool A)

        proof

          let x be object;

          assume x in F;

          then

          consider C be Subset of X such that

           A3: x = C and

           A4: ex a be Point of X st a in A & C = {a};

          C c= A by A4, ZFMISC_1: 31;

          hence thesis by A3;

        end;

        ( bool A) c= ( bool the carrier of X) by ZFMISC_1: 67;

        then

        reconsider F as Subset-Family of X by A2, XBOOLE_1: 1;



         A5: ( union ( bool A)) = A by ZFMISC_1: 81;

        now

          let x be set;

          assume

           A6: x in ( bool A);

          then

          reconsider P = x as Subset of X by XBOOLE_1: 1;

          now

            let y be object;

            assume

             A7: y in P;

            then

            reconsider a = y as Point of X;

            now

              take B0 = {a};

              B0 is Subset of X by A7, ZFMISC_1: 31;

              hence y in B0 & B0 in F by A6, A7, TARSKI:def 1;

            end;

            hence y in ( union F) by TARSKI:def 4;

          end;

          hence x c= ( union F);

        end;

        then

         A8: ( union ( bool A)) c= ( union F);

        now

          let B be Subset of X;

          assume B in F;

          then ex C be Subset of X st C = B & ex a be Point of X st a in A & C = {a};

          hence B is open by A1;

        end;

        then

         A9: F is open by TOPS_2:def 1;

        ( union F) c= ( union ( bool A)) by A2, ZFMISC_1: 77;

        then ( union F) = A by A8, A5;

        hence A is open by A9, TOPS_2: 19;

      end;

      hence thesis by Th15;

    end;

    registration

      let X be discrete non empty TopSpace;

      cluster -> open closed discrete for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        thus X0 is open by Th15;

        thus X0 is closed by Th16;



         A1: the topology of X = ( bool the carrier of X) by Def1;

        now

          let S be object;

          assume S in ( bool the carrier of X0);

          then

          reconsider A = S as Subset of X0;

          the carrier of X0 c= the carrier of X by BORSUK_1: 1;

          then

          reconsider B = A as Subset of X by XBOOLE_1: 1;

          now

            take B;

            thus B in the topology of X & A = (B /\ ( [#] X0)) by A1, XBOOLE_1: 28;

          end;

          hence S in the topology of X0 by PRE_TOPC:def 4;

        end;

        then ( bool the carrier of X0) c= the topology of X0;

        hence the topology of X0 = ( bool the carrier of X0);

      end;

    end

    registration

      let X be discrete non empty TopSpace;

      cluster discrete strict for SubSpace of X;

      existence

      proof

        set X0 = the strict SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    theorem :: TDLAT_3:18



     Th18: X is anti-discrete iff for A be Subset of X st A is open holds A = {} or A = the carrier of X

    proof



       A1: the carrier of X in the topology of X by PRE_TOPC:def 1;

      thus X is anti-discrete implies for A be Subset of X st A is open holds A = {} or A = the carrier of X

      proof

        assume

         A2: X is anti-discrete;

        let A be Subset of X;

        assume A is open;

        then A in the topology of X by PRE_TOPC:def 2;

        then A in { {} , the carrier of X} by A2;

        hence thesis by TARSKI:def 2;

      end;

      assume

       A3: for A be Subset of X st A is open holds A = {} or A = the carrier of X;

      now

        let P be object;

        assume

         A4: P in the topology of X;

        then

        reconsider C = P as Subset of X;

        C is open by A4, PRE_TOPC:def 2;

        then C = {} or C = the carrier of X by A3;

        hence P in { {} , the carrier of X} by TARSKI:def 2;

      end;

      then

       A5: the topology of X c= { {} , the carrier of X};

       {} in the topology of X by PRE_TOPC: 1;

      then { {} , the carrier of X} c= the topology of X by A1, ZFMISC_1: 32;

      then the topology of X = { {} , the carrier of X} by A5;

      hence thesis;

    end;

    theorem :: TDLAT_3:19



     Th19: X is anti-discrete iff for A be Subset of X st A is closed holds A = {} or A = the carrier of X

    proof

      thus X is anti-discrete implies for A be Subset of X st A is closed holds A = {} or A = the carrier of X

      proof

        assume

         A1: X is anti-discrete;

        let A be Subset of X;

        assume A is closed;

        then (A ` ) = {} or (A ` ) = the carrier of X by A1, Th18;

        then ((A ` ) ` ) = ( [#] X) or ((A ` ) ` ) = ( {} X) by XBOOLE_1: 37;

        hence thesis;

      end;

      assume

       A2: for A be Subset of X st A is closed holds A = {} or A = the carrier of X;

      now

        let B be Subset of X;

        assume B is open;

        then (B ` ) = {} or (B ` ) = the carrier of X by A2;

        then ((B ` ) ` ) = ( [#] X) or ((B ` ) ` ) = ( {} X) by XBOOLE_1: 37;

        hence B = {} or B = the carrier of X;

      end;

      hence thesis by Th18;

    end;

    theorem :: TDLAT_3:20

    (for A be Subset of X, x be Point of X st A = {x} holds ( Cl A) = the carrier of X) implies X is anti-discrete

    proof

      assume

       A1: for A be Subset of X, x be Point of X st A = {x} holds ( Cl A) = the carrier of X;

      for B be Subset of X st B is closed holds B = {} or B = the carrier of X

      proof

        let B be Subset of X;

        assume

         A2: B is closed;

        set z = the Element of B;

        assume

         A3: B <> {} ;

        then

        reconsider x = z as Point of X by TARSKI:def 3;



         A4: {x} c= B by A3, ZFMISC_1: 31;

        then

        reconsider A = {x} as Subset of X by XBOOLE_1: 1;

        ( Cl A) = the carrier of X by A1;

        then the carrier of X c= B by A2, A4, TOPS_1: 5;

        hence thesis;

      end;

      hence thesis by Th19;

    end;

    registration

      let X be anti-discrete non empty TopSpace;

      cluster -> anti-discrete for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;



         A1: the topology of X = { {} , the carrier of X} by Def2;

        now

          let S be object;

          assume

           A2: S in the topology of X0;

          then

          reconsider A = S as Subset of X0;

          consider B be Subset of X such that

           A3: B in the topology of X and

           A4: A = (B /\ ( [#] X0)) by A2, PRE_TOPC:def 4;



           A5: B = the carrier of X implies A = the carrier of X0 by A4, BORSUK_1: 1, XBOOLE_1: 28;

          B = {} implies A = {} by A4;

          hence S in { {} , the carrier of X0} by A1, A3, A5, TARSKI:def 2;

        end;

        then

         A6: the topology of X0 c= { {} , the carrier of X0};

        now

          let S be object;

          assume S in { {} , the carrier of X0};

          then S = {} or S = the carrier of X0 by TARSKI:def 2;

          hence S in the topology of X0 by PRE_TOPC: 1, PRE_TOPC:def 1;

        end;

        then { {} , the carrier of X0} c= the topology of X0;

        then the topology of X0 = { {} , the carrier of X0} by A6;

        hence thesis;

      end;

    end

    registration

      let X be anti-discrete non empty TopSpace;

      cluster anti-discrete for SubSpace of X;

      existence

      proof

        set X0 = the SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    theorem :: TDLAT_3:21



     Th21: X is almost_discrete iff for A be Subset of X st A is open holds A is closed

    proof

      thus X is almost_discrete implies for A be Subset of X st A is open holds A is closed

      proof

        assume

         A1: X is almost_discrete;

        now

          let A be Subset of X;

          assume A is open;

          then A in the topology of X by PRE_TOPC:def 2;

          then (the carrier of X \ A) in the topology of X by A1;

          then (( [#] X) \ A) is open by PRE_TOPC:def 2;

          hence A is closed by PRE_TOPC:def 3;

        end;

        hence thesis;

      end;

      assume

       A2: for A be Subset of X st A is open holds A is closed;

      now

        let A be Subset of X;

        reconsider A9 = A as Subset of X;

        assume A in the topology of X;

        then A9 is open by PRE_TOPC:def 2;

        then A9 is closed by A2;

        then (( [#] X) \ A9) is open by PRE_TOPC:def 3;

        hence (the carrier of X \ A) in the topology of X by PRE_TOPC:def 2;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_3:22



     Th22: X is almost_discrete iff for A be Subset of X st A is closed holds A is open

    proof

      thus X is almost_discrete implies for A be Subset of X st A is closed holds A is open

      proof

        assume

         A1: X is almost_discrete;

        let A be Subset of X;

        assume A is closed;

        then (A ` ) is closed by A1, Th21;

        hence thesis by TOPS_1: 4;

      end;

      assume

       A2: for A be Subset of X st A is closed holds A is open;

      now

        let A be Subset of X;

        assume A is open;

        then (A ` ) is open by A2;

        hence A is closed by TOPS_1: 3;

      end;

      hence thesis by Th21;

    end;

    theorem :: TDLAT_3:23

    X is almost_discrete iff for A be Subset of X st A is open holds ( Cl A) = A

    proof

      thus X is almost_discrete implies for A be Subset of X st A is open holds ( Cl A) = A by Th21, PRE_TOPC: 22;

      assume

       A1: for A be Subset of X st A is open holds ( Cl A) = A;

      now

        let A be Subset of X;

        assume A is open;

        then ( Cl A) = A by A1;

        hence A is closed;

      end;

      hence thesis by Th21;

    end;

    theorem :: TDLAT_3:24

    X is almost_discrete iff for A be Subset of X st A is closed holds ( Int A) = A

    proof

      thus X is almost_discrete implies for A be Subset of X st A is closed holds ( Int A) = A by Th22, TOPS_1: 23;

      assume

       A1: for A be Subset of X st A is closed holds ( Int A) = A;

      now

        let A be Subset of X;

        assume A is closed;

        then ( Int A) = A by A1;

        hence A is open;

      end;

      hence thesis by Th22;

    end;

    registration

      cluster almost_discrete strict for TopSpace;

      existence

      proof

        set X = the discrete strict TopSpace;

        take X;

        thus thesis;

      end;

    end

    theorem :: TDLAT_3:25

    (for A be Subset of X, x be Point of X st A = {x} holds ( Cl A) is open) implies X is almost_discrete

    proof

      assume

       A1: for D be Subset of X, x be Point of X st D = {x} holds ( Cl D) is open;

      for A be Subset of X st A is closed holds A is open

      proof

        let A be Subset of X;

        set F = { B where B be Subset of X : ex C be Subset of X, a be Point of X st a in A & C = {a} & B = ( Cl C) };



         A2: ( union ( bool A)) = A by ZFMISC_1: 81;

        assume

         A3: A is closed;



         A4: for C be Subset of X, a be Point of X st a in A & C = {a} holds ( Cl C) c= A

        proof

          let C be Subset of X, a be Point of X;

          assume that

           A5: a in A and

           A6: C = {a};

          C c= A by A5, A6, ZFMISC_1: 31;

          then ( Cl C) c= ( Cl A) by PRE_TOPC: 19;

          hence thesis by A3, PRE_TOPC: 22;

        end;



         A7: F c= ( bool A)

        proof

          let x be object;

          assume x in F;

          then

          consider P be Subset of X such that

           A8: x = P and

           A9: ex C be Subset of X, a be Point of X st a in A & C = {a} & P = ( Cl C);

          P c= A by A4, A9;

          hence thesis by A8;

        end;

        ( bool A) c= ( bool the carrier of X) by ZFMISC_1: 67;

        then

        reconsider F as Subset-Family of X by A7, XBOOLE_1: 1;

        now

          let x be set;

          assume

           A10: x in ( bool A);

          then

          reconsider P = x as Subset of X by XBOOLE_1: 1;

          now

            let y be object;

            assume

             A11: y in P;

            then

            reconsider a = y as Point of X;

            now

              reconsider P0 = {a} as Subset of X by A11, ZFMISC_1: 31;

              take B = ( Cl P0);



               A12: P0 c= B by PRE_TOPC: 18;

              a in P0 by TARSKI:def 1;

              hence y in B & B in F by A10, A11, A12;

            end;

            hence y in ( union F) by TARSKI:def 4;

          end;

          hence x c= ( union F);

        end;

        then

         A13: ( union ( bool A)) c= ( union F);

        now

          let D be Subset of X;

          assume D in F;

          then ex S be Subset of X st S = D & ex C be Subset of X, a be Point of X st a in A & C = {a} & S = ( Cl C);

          hence D is open by A1;

        end;

        then

         A14: F is open by TOPS_2:def 1;

        ( union F) c= ( union ( bool A)) by A7, ZFMISC_1: 77;

        then ( union F) = A by A13, A2;

        hence thesis by A14, TOPS_2: 19;

      end;

      hence thesis by Th22;

    end;

    theorem :: TDLAT_3:26

    X is discrete iff X is almost_discrete & for A be Subset of X, x be Point of X st A = {x} holds A is closed

    proof

      thus X is discrete implies X is almost_discrete & for A be Subset of X, x be Point of X st A = {x} holds A is closed by Th16;

      assume

       A1: X is almost_discrete;

      assume

       A2: for A be Subset of X, x be Point of X st A = {x} holds A is closed;

      for A be Subset of X, x be Point of X st A = {x} holds A is open by A2, A1, Th22;

      hence thesis by Th17;

    end;

    registration

      cluster discrete -> almost_discrete for TopSpace;

      coherence ;

      cluster anti-discrete -> almost_discrete for TopSpace;

      coherence ;

    end

    registration

      let X be almost_discrete non empty TopSpace;

      cluster -> almost_discrete for non empty SubSpace of X;

      coherence

      proof

        let X0 be non empty SubSpace of X;

        now

          let A0 be Subset of X0;

          assume A0 is open;

          then

          consider A be Subset of X such that

           A1: A is open and

           A2: A0 = (A /\ ( [#] X0)) by TOPS_2: 24;

          A is closed by A1, Th21;

          hence A0 is closed by A2, PRE_TOPC: 13;

        end;

        hence thesis by Th21;

      end;

    end

    registration

      let X be almost_discrete non empty TopSpace;

      cluster open -> closed for SubSpace of X;

      coherence by Th21;

      cluster closed -> open for SubSpace of X;

      coherence by Th22;

    end

    registration

      let X be almost_discrete non empty TopSpace;

      cluster almost_discrete strict non empty for SubSpace of X;

      existence

      proof

        set X0 = the strict non empty SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    begin

    definition

      let IT be non empty TopSpace;

      :: TDLAT_3:def4

      attr IT is extremally_disconnected means

      : Def4: for A be Subset of IT st A is open holds ( Cl A) is open;

    end

    registration

      cluster extremally_disconnected strict for non empty TopSpace;

      existence

      proof

        set X = the discrete strict non empty TopSpace;

        take X;

        for A be Subset of X st A is open holds ( Cl A) is open by PRE_TOPC: 22, Th16;

        hence thesis;

      end;

    end

    reserve X for non empty TopSpace;

    theorem :: TDLAT_3:27



     Th27: X is extremally_disconnected iff for A be Subset of X st A is closed holds ( Int A) is closed

    proof

      thus X is extremally_disconnected implies for A be Subset of X st A is closed holds ( Int A) is closed

      proof

        assume

         A1: X is extremally_disconnected;

        let A be Subset of X;

        assume A is closed;

        then ( Cl (A ` )) is open by A1;

        then (( Cl (A ` )) ` ) is closed;

        hence thesis by TOPS_1:def 1;

      end;

      assume

       A2: for A be Subset of X st A is closed holds ( Int A) is closed;

      now

        let A be Subset of X;

        assume A is open;

        then ( Int (A ` )) is closed by A2;

        then (( Int (A ` )) ` ) is open;

        hence ( Cl A) is open by Th1;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_3:28



     Th28: X is extremally_disconnected iff for A,B be Subset of X st A is open & B is open holds A misses B implies ( Cl A) misses ( Cl B)

    proof

      thus X is extremally_disconnected implies for A,B be Subset of X st A is open & B is open holds A misses B implies ( Cl A) misses ( Cl B)

      proof

        assume

         A1: X is extremally_disconnected;

        let A,B be Subset of X;

        assume that

         A2: A is open and

         A3: B is open;

        assume A misses B;

        then

         A4: A misses ( Cl B) by A2, TSEP_1: 36;

        ( Cl B) is open by A1, A3;

        hence thesis by A4, TSEP_1: 36;

      end;

      assume

       A5: for A,B be Subset of X st A is open & B is open holds A misses B implies ( Cl A) misses ( Cl B);

      now

        let A be Subset of X;

        A c= ( Cl A) by PRE_TOPC: 18;

        then

         A6: A misses (( Cl A) ` ) by SUBSET_1: 24;

        assume A is open;

        then ( Cl A) misses ( Cl (( Cl A) ` )) by A5, A6;

        then ( Cl A) c= (( Cl (( Cl A) ` )) ` ) by SUBSET_1: 23;

        then

         A7: ( Cl A) c= ( Int ( Cl A)) by TOPS_1:def 1;

        ( Int ( Cl A)) c= ( Cl A) by TOPS_1: 16;

        hence ( Cl A) is open by A7, XBOOLE_0:def 10;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_3:29

    X is extremally_disconnected iff for A,B be Subset of X st A is closed & B is closed holds (A \/ B) = the carrier of X implies (( Int A) \/ ( Int B)) = the carrier of X

    proof

      thus X is extremally_disconnected implies for A,B be Subset of X st A is closed & B is closed holds (A \/ B) = the carrier of X implies (( Int A) \/ ( Int B)) = the carrier of X

      proof

        assume

         A1: X is extremally_disconnected;

        let A,B be Subset of X;

        assume that

         A2: A is closed and

         A3: B is closed;

        assume (A \/ B) = the carrier of X;

        then ((A \/ B) ` ) = ( {} X) by XBOOLE_1: 37;

        then ((A ` ) /\ (B ` )) = ( {} X) by XBOOLE_1: 53;

        then (A ` ) misses (B ` );

        then ( Cl (A ` )) misses ( Cl (B ` )) by A1, A2, A3, Th28;

        then (( Cl (A ` )) /\ ( Cl (B ` ))) = ( {} X);

        then ((( Cl (A ` )) /\ ( Cl (B ` ))) ` ) = ( [#] X);

        then ((( Cl (A ` )) ` ) \/ (( Cl (B ` )) ` )) = ( [#] X) by XBOOLE_1: 54;

        then ((( Cl (A ` )) ` ) \/ ( Int B)) = ( [#] X) by TOPS_1:def 1;

        hence thesis by TOPS_1:def 1;

      end;

      assume

       A4: for A,B be Subset of X st A is closed & B is closed holds (A \/ B) = the carrier of X implies (( Int A) \/ ( Int B)) = the carrier of X;

      now

        let A,B be Subset of X;

        assume that

         A5: A is open and

         A6: B is open;

        assume A misses B;

        then (A /\ B) = ( {} X);

        then ((A /\ B) ` ) = ( [#] X);

        then ((A ` ) \/ (B ` )) = ( [#] X) by XBOOLE_1: 54;

        then (( Int (A ` )) \/ ( Int (B ` ))) = the carrier of X by A4, A5, A6;

        then ((( Int (A ` )) \/ ( Int (B ` ))) ` ) = ( {} X) by XBOOLE_1: 37;

        then ((( Int (A ` )) ` ) /\ (( Int (B ` )) ` )) = ( {} X) by XBOOLE_1: 53;

        then (( Cl A) /\ (( Int (B ` )) ` )) = ( {} X) by Th1;

        then ( Cl A) misses (( Int (B ` )) ` );

        hence ( Cl A) misses ( Cl B) by Th1;

      end;

      hence thesis by Th28;

    end;

    theorem :: TDLAT_3:30



     Th30: X is extremally_disconnected iff for A be Subset of X st A is open holds ( Cl A) = ( Int ( Cl A))

    proof

      thus X is extremally_disconnected implies for A be Subset of X st A is open holds ( Cl A) = ( Int ( Cl A))

      proof

        assume

         A1: X is extremally_disconnected;

        let A be Subset of X;

        A c= ( Cl A) by PRE_TOPC: 18;

        then

         A2: A misses (( Cl A) ` ) by SUBSET_1: 24;

        assume A is open;

        then ( Cl A) misses ( Cl (( Cl A) ` )) by A1, A2, Th28;

        then ( Cl A) c= (( Cl (( Cl A) ` )) ` ) by SUBSET_1: 23;

        then

         A3: ( Cl A) c= ( Int ( Cl A)) by TOPS_1:def 1;

        ( Int ( Cl A)) c= ( Cl A) by TOPS_1: 16;

        hence thesis by A3;

      end;

      assume

       A4: for A be Subset of X st A is open holds ( Cl A) = ( Int ( Cl A));

      now

        let A be Subset of X;

        assume A is open;

        then ( Cl A) = ( Int ( Cl A)) by A4;

        hence ( Cl A) is open;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_3:31

    X is extremally_disconnected iff for A be Subset of X st A is closed holds ( Int A) = ( Cl ( Int A))

    proof

      thus X is extremally_disconnected implies for A be Subset of X st A is closed holds ( Int A) = ( Cl ( Int A))

      proof

        assume

         A1: X is extremally_disconnected;

        let A be Subset of X;

        assume A is closed;

        then ( Cl (A ` )) = ( Int ( Cl (A ` ))) by A1, Th30;

        then ( Int A) = (( Int ((( Cl (A ` )) ` ) ` )) ` ) by TOPS_1:def 1;

        then ( Int A) = ( Cl (( Cl (A ` )) ` )) by Th1;

        hence thesis;

      end;

      assume

       A2: for A be Subset of X st A is closed holds ( Int A) = ( Cl ( Int A));

      now

        let A be Subset of X;

        assume A is closed;

        then ( Int A) = ( Cl ( Int A)) by A2;

        hence ( Int A) is closed;

      end;

      hence thesis by Th27;

    end;

    theorem :: TDLAT_3:32



     Th32: X is extremally_disconnected iff for A be Subset of X st A is condensed holds A is closed & A is open

    proof

      thus X is extremally_disconnected implies for A be Subset of X st A is condensed holds A is closed & A is open

      proof

        assume

         A1: X is extremally_disconnected;

        let A be Subset of X;



         A2: ( Cl ( Int A)) is open by A1;

        assume

         A3: A is condensed;

        then ( Cl A) = ( Cl ( Int A)) by Th9;

        then ( Int ( Cl A)) = ( Cl ( Int A)) by A2, TOPS_1: 23;

        hence thesis by A3, Th8;

      end;

      assume

       A4: for A be Subset of X st A is condensed holds A is closed & A is open;

      now

        let A be Subset of X;

        assume A is open;

        then

         A5: ( Int A) = A by TOPS_1: 23;

        ( Cl ( Int A)) is closed_condensed by TDLAT_1: 22;

        then ( Cl A) is condensed by A5, TOPS_1: 66;

        hence ( Cl A) is open by A4;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_3:33



     Th33: X is extremally_disconnected iff for A be Subset of X st A is condensed holds A is closed_condensed & A is open_condensed

    proof

      thus X is extremally_disconnected implies for A be Subset of X st A is condensed holds A is closed_condensed & A is open_condensed by Th32, TOPS_1: 66, TOPS_1: 67;

      assume

       A1: for A be Subset of X st A is condensed holds A is closed_condensed & A is open_condensed;

      now

        let A be Subset of X;

        assume

         A2: A is condensed;

        then

         A3: A is open_condensed by A1;

        A is closed_condensed by A1, A2;

        hence A is closed & A is open by A3, TOPS_1: 66, TOPS_1: 67;

      end;

      hence thesis by Th32;

    end;

    theorem :: TDLAT_3:34



     Th34: X is extremally_disconnected iff for A be Subset of X st A is condensed holds ( Int ( Cl A)) = ( Cl ( Int A))

    proof

      thus X is extremally_disconnected implies for A be Subset of X st A is condensed holds ( Int ( Cl A)) = ( Cl ( Int A))

      proof

        assume

         A1: X is extremally_disconnected;

        let A be Subset of X;

        assume A is condensed;

        then

         A2: ( Cl A) = ( Cl ( Int A)) by Th9;

        ( Cl ( Int A)) is open by A1;

        hence thesis by A2, TOPS_1: 23;

      end;

      assume

       A3: for A be Subset of X st A is condensed holds ( Int ( Cl A)) = ( Cl ( Int A));

      now

        let A be Subset of X;

        assume

         A4: A is condensed;

        then ( Int ( Cl A)) = ( Cl ( Int A)) by A3;

        hence A is closed & A is open by A4, Th8;

      end;

      hence thesis by Th32;

    end;

    theorem :: TDLAT_3:35

    X is extremally_disconnected iff for A be Subset of X st A is condensed holds ( Int A) = ( Cl A)

    proof

      thus X is extremally_disconnected implies for A be Subset of X st A is condensed holds ( Int A) = ( Cl A)

      proof

        assume

         A1: X is extremally_disconnected;

        let A be Subset of X;

        assume

         A2: A is condensed;

        then A is closed by A1, Th32;

        then

         A3: A = ( Cl A) by PRE_TOPC: 22;

        A is open by A1, A2, Th32;

        hence thesis by A3, TOPS_1: 23;

      end;

      assume

       A4: for A be Subset of X st A is condensed holds ( Int A) = ( Cl A);

      now

        let A be Subset of X;

        assume A is condensed;

        then ( Int A) = ( Cl A) by A4;

        hence A is closed & A is open by Th5;

      end;

      hence thesis by Th32;

    end;

    theorem :: TDLAT_3:36



     Th36: X is extremally_disconnected iff for A be Subset of X holds (A is open_condensed implies A is closed_condensed) & (A is closed_condensed implies A is open_condensed)

    proof

      thus X is extremally_disconnected implies for A be Subset of X holds (A is open_condensed implies A is closed_condensed) & (A is closed_condensed implies A is open_condensed)

      proof

        assume

         A1: X is extremally_disconnected;

        let A be Subset of X;

        thus A is open_condensed implies A is closed_condensed

        proof

          assume A is open_condensed;

          then A is condensed by TOPS_1: 67;

          hence thesis by A1, Th33;

        end;

        thus A is closed_condensed implies A is open_condensed

        proof

          assume A is closed_condensed;

          then A is condensed by TOPS_1: 66;

          hence thesis by A1, Th33;

        end;

      end;

      assume

       A2: for A be Subset of X holds (A is open_condensed implies A is closed_condensed) & (A is closed_condensed implies A is open_condensed);

      for A be Subset of X st A is condensed holds ( Int ( Cl A)) = ( Cl ( Int A))

      proof

        let A be Subset of X;

        assume

         A3: A is condensed;

        then

         A4: A c= ( Cl ( Int A)) by TOPS_1:def 6;

        ( Cl ( Int A)) is closed_condensed by TDLAT_1: 22;

        then ( Cl ( Int A)) is open_condensed by A2;

        then ( Cl ( Int A)) = ( Int ( Cl ( Cl ( Int A)))) by TOPS_1:def 8;

        then

         A5: ( Cl ( Int A)) c= ( Int ( Cl A)) by TDLAT_2: 1;

        ( Int ( Cl A)) c= A by A3, TOPS_1:def 6;

        then ( Int ( Cl A)) c= ( Cl ( Int A)) by A4;

        hence thesis by A5;

      end;

      hence thesis by Th34;

    end;

    definition

      let IT be non empty TopSpace;

      :: TDLAT_3:def5

      attr IT is hereditarily_extremally_disconnected means

      : Def5: for X0 be non empty SubSpace of IT holds X0 is extremally_disconnected;

    end

    registration

      cluster hereditarily_extremally_disconnected strict for non empty TopSpace;

      existence

      proof

        take X = the discrete strict non empty TopSpace;

        for X0 be non empty SubSpace of X holds X0 is extremally_disconnected by Th16, PRE_TOPC: 22;

        hence thesis;

      end;

    end

    registration

      cluster hereditarily_extremally_disconnected -> extremally_disconnected for non empty TopSpace;

      coherence

      proof

        let X be non empty TopSpace such that

         A1: X is hereditarily_extremally_disconnected;

        X is SubSpace of X by TSEP_1: 2;

        hence thesis by A1;

      end;

      cluster almost_discrete -> hereditarily_extremally_disconnected for non empty TopSpace;

      coherence

      proof

        let X be non empty TopSpace;

        assume X is almost_discrete;

        then

        reconsider X as almost_discrete non empty TopSpace;

        for X0 be non empty SubSpace of X holds X0 is extremally_disconnected by Th21, PRE_TOPC: 22;

        hence thesis;

      end;

    end

    theorem :: TDLAT_3:37



     Th37: for X be extremally_disconnected non empty TopSpace, X0 be non empty SubSpace of X, A be Subset of X st A = the carrier of X0 & A is dense holds X0 is extremally_disconnected

    proof

      let X be extremally_disconnected non empty TopSpace, X0 be non empty SubSpace of X, A be Subset of X;

      assume

       A1: A = the carrier of X0;

      assume

       A2: A is dense;

      for D0,B0 be Subset of X0 st D0 is open & B0 is open holds D0 misses B0 implies ( Cl D0) misses ( Cl B0)

      proof

        let D0,B0 be Subset of X0;

        assume that

         A3: D0 is open and

         A4: B0 is open;

        consider D be Subset of X such that

         A5: D is open and

         A6: (D /\ ( [#] X0)) = D0 by A3, TOPS_2: 24;

        consider B be Subset of X such that

         A7: B is open and

         A8: (B /\ ( [#] X0)) = B0 by A4, TOPS_2: 24;

        assume

         A9: (D0 /\ B0) = {} ;

        D misses B

        proof

          assume (D /\ B) <> {} ;

          then (D /\ B) meets A by A2, A5, A7, TOPS_1: 45;

          then ((D /\ B) /\ A) <> {} ;

          then (D /\ (B /\ (A /\ A))) <> {} by XBOOLE_1: 16;

          then (D /\ (A /\ (B /\ A))) <> {} by XBOOLE_1: 16;

          hence contradiction by A1, A6, A8, A9, XBOOLE_1: 16;

        end;

        then ( Cl D) misses ( Cl B) by A5, A7, Th28;

        then (( Cl D) /\ ( Cl B)) = {} ;

        then ((( Cl D) /\ ( Cl B)) /\ ( [#] X0)) = {} ;

        then (( Cl D) /\ (( Cl B) /\ (( [#] X0) /\ ( [#] X0)))) = {} by XBOOLE_1: 16;

        then (( Cl D) /\ (( [#] X0) /\ (( Cl B) /\ ( [#] X0)))) = {} by XBOOLE_1: 16;

        then

         A10: ((( Cl D) /\ ( [#] X0)) /\ (( Cl B) /\ ( [#] X0))) = {} by XBOOLE_1: 16;



         A11: ( Cl B0) c= (( Cl B) /\ ( [#] X0))

        proof

          B0 c= B by A8, XBOOLE_1: 17;

          then

          reconsider B1 = B0 as Subset of X by XBOOLE_1: 1;

          ( Cl B1) c= ( Cl B) by A8, PRE_TOPC: 19, XBOOLE_1: 17;

          then (( Cl B1) /\ ( [#] X0)) c= (( Cl B) /\ ( [#] X0)) by XBOOLE_1: 26;

          hence thesis by PRE_TOPC: 17;

        end;

        ( Cl D0) c= (( Cl D) /\ ( [#] X0))

        proof

          D0 c= D by A6, XBOOLE_1: 17;

          then

          reconsider D1 = D0 as Subset of X by XBOOLE_1: 1;

          ( Cl D1) c= ( Cl D) by A6, PRE_TOPC: 19, XBOOLE_1: 17;

          then (( Cl D1) /\ ( [#] X0)) c= (( Cl D) /\ ( [#] X0)) by XBOOLE_1: 26;

          hence thesis by PRE_TOPC: 17;

        end;

        then (( Cl D0) /\ ( Cl B0)) c= ((( Cl D) /\ ( [#] X0)) /\ (( Cl B) /\ ( [#] X0))) by A11, XBOOLE_1: 27;

        then (( Cl D0) /\ ( Cl B0)) = {} by A10;

        hence thesis;

      end;

      hence thesis by Th28;

    end;

    registration

      let X be extremally_disconnected non empty TopSpace;

      cluster open -> extremally_disconnected for non empty SubSpace of X;

      coherence

      proof

        let X0 be non empty SubSpace of X such that

         A1: X0 is open;

        reconsider B = the carrier of X0 as Subset of X by TSEP_1: 1;

        now

          let A0 be Subset of X0;

          A0 c= B;

          then

          reconsider A = A0 as Subset of X by XBOOLE_1: 1;

          assume A0 is open;

          then A is open by A1, TSEP_1: 17;

          then

           A2: ( Cl A) is open by Def4;

          ( Cl A0) = (( Cl A) /\ ( [#] X0)) by PRE_TOPC: 17;

          hence ( Cl A0) is open by A2, TOPS_2: 24;

        end;

        hence thesis;

      end;

    end

    registration

      let X be extremally_disconnected non empty TopSpace;

      cluster extremally_disconnected strict for non empty SubSpace of X;

      existence

      proof

        set X0 = the strict open non empty SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    registration

      let X be hereditarily_extremally_disconnected non empty TopSpace;

      cluster -> hereditarily_extremally_disconnected for non empty SubSpace of X;

      coherence

      proof

        let X0 be non empty SubSpace of X;

        for Y be non empty SubSpace of X0 holds Y is extremally_disconnected

        proof

          let Y be non empty SubSpace of X0;

          Y is SubSpace of X by TSEP_1: 7;

          hence thesis by Def5;

        end;

        hence thesis;

      end;

    end

    registration

      let X be hereditarily_extremally_disconnected non empty TopSpace;

      cluster hereditarily_extremally_disconnected strict for non empty SubSpace of X;

      existence

      proof

        set X0 = the strict non empty SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    theorem :: TDLAT_3:38

    (for X0 be closed non empty SubSpace of X holds X0 is extremally_disconnected) implies X is hereditarily_extremally_disconnected

    proof

      assume

       A1: for Y be closed non empty SubSpace of X holds Y is extremally_disconnected;

      for X0 be non empty SubSpace of X holds X0 is extremally_disconnected

      proof

        let X0 be non empty SubSpace of X;

        reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

        set A = ( Cl A0);

        A is non empty by PCOMPS_1: 2;

        then

        consider Y be strict closed non empty SubSpace of X such that

         A2: A = the carrier of Y by TSEP_1: 15;

        A0 c= A by PRE_TOPC: 18;

        then

        reconsider Y0 = X0 as non empty SubSpace of Y by A2, TSEP_1: 4;

        reconsider B0 = the carrier of Y0 as Subset of Y by TSEP_1: 1;

        ( Cl B0) = (A /\ ( [#] Y)) by PRE_TOPC: 17;

        then

         A3: B0 is dense by A2, TOPS_1:def 3;

        Y is extremally_disconnected by A1;

        hence thesis by A3, Th37;

      end;

      hence thesis;

    end;

    begin

    reserve Y for extremally_disconnected non empty TopSpace;

    theorem :: TDLAT_3:39



     Th39: ( Domains_of Y) = ( Closed_Domains_of Y)

    proof

      now

        let S be object;

        assume

         A1: S in ( Domains_of Y);

        then

        reconsider A = S as Subset of Y;

        A in { D where D be Subset of Y : D is condensed } by A1;

        then ex D be Subset of Y st D = A & D is condensed;

        then A is closed_condensed by Th33;

        then A in { E where E be Subset of Y : E is closed_condensed };

        hence S in ( Closed_Domains_of Y);

      end;

      then

       A2: ( Domains_of Y) c= ( Closed_Domains_of Y);

      ( Closed_Domains_of Y) c= ( Domains_of Y) by TDLAT_1: 31;

      hence thesis by A2;

    end;

    theorem :: TDLAT_3:40



     Th40: ( D-Union Y) = ( CLD-Union Y) & ( D-Meet Y) = ( CLD-Meet Y)

    proof



       A1: ( Domains_of Y) = ( Closed_Domains_of Y) by Th39;



      hence ( D-Union Y) = (( D-Union Y) || ( Closed_Domains_of Y)) by RELSET_1: 19

      .= ( CLD-Union Y) by TDLAT_1: 39;



      thus ( D-Meet Y) = (( D-Meet Y) || ( Closed_Domains_of Y)) by A1, RELSET_1: 19

      .= ( CLD-Meet Y) by TDLAT_1: 40;

    end;

    theorem :: TDLAT_3:41



     Th41: ( Domains_Lattice Y) = ( Closed_Domains_Lattice Y)

    proof



       A1: ( D-Union Y) = ( CLD-Union Y) by Th40;



       A2: ( D-Meet Y) = ( CLD-Meet Y) by Th40;

      ( Domains_of Y) = ( Closed_Domains_of Y) by Th39;



      hence ( Domains_Lattice Y) = LattStr (# ( Closed_Domains_of Y), ( CLD-Union Y), ( CLD-Meet Y) #) by A1, A2

      .= ( Closed_Domains_Lattice Y);

    end;

    theorem :: TDLAT_3:42



     Th42: ( Domains_of Y) = ( Open_Domains_of Y)

    proof

      now

        let S be object;

        assume

         A1: S in ( Domains_of Y);

        then

        reconsider A = S as Subset of Y;

        A in { D where D be Subset of Y : D is condensed } by A1;

        then ex D be Subset of Y st D = A & D is condensed;

        then A is open_condensed by Th33;

        then A in { E where E be Subset of Y : E is open_condensed };

        hence S in ( Open_Domains_of Y);

      end;

      then

       A2: ( Domains_of Y) c= ( Open_Domains_of Y);

      ( Open_Domains_of Y) c= ( Domains_of Y) by TDLAT_1: 35;

      hence thesis by A2;

    end;

    theorem :: TDLAT_3:43



     Th43: ( D-Union Y) = ( OPD-Union Y) & ( D-Meet Y) = ( OPD-Meet Y)

    proof



       A1: ( Domains_of Y) = ( Open_Domains_of Y) by Th42;



      hence ( D-Union Y) = (( D-Union Y) || ( Open_Domains_of Y)) by RELSET_1: 19

      .= ( OPD-Union Y) by TDLAT_1: 42;



      thus ( D-Meet Y) = (( D-Meet Y) || ( Open_Domains_of Y)) by A1, RELSET_1: 19

      .= ( OPD-Meet Y) by TDLAT_1: 43;

    end;

    theorem :: TDLAT_3:44



     Th44: ( Domains_Lattice Y) = ( Open_Domains_Lattice Y)

    proof



       A1: ( D-Union Y) = ( OPD-Union Y) by Th43;



       A2: ( D-Meet Y) = ( OPD-Meet Y) by Th43;

      ( Domains_of Y) = ( Open_Domains_of Y) by Th42;



      hence ( Domains_Lattice Y) = LattStr (# ( Open_Domains_of Y), ( OPD-Union Y), ( OPD-Meet Y) #) by A1, A2

      .= ( Open_Domains_Lattice Y);

    end;

    theorem :: TDLAT_3:45



     Th45: for A,B be Element of ( Domains_of Y) holds (( D-Union Y) . (A,B)) = (A \/ B) & (( D-Meet Y) . (A,B)) = (A /\ B)

    proof

      let A,B be Element of ( Domains_of Y);

      reconsider A0 = A, B0 = B as Element of ( Closed_Domains_of Y) by Th39;

      (( D-Union Y) . (A,B)) = (( CLD-Union Y) . (A0,B0)) by Th40;

      hence (( D-Union Y) . (A,B)) = (A \/ B) by TDLAT_1:def 6;

      reconsider A0 = A, B0 = B as Element of ( Open_Domains_of Y) by Th42;

      (( D-Meet Y) . (A,B)) = (( OPD-Meet Y) . (A0,B0)) by Th43;

      hence thesis by TDLAT_1:def 11;

    end;

    theorem :: TDLAT_3:46

    for a,b be Element of ( Domains_Lattice Y) holds for A,B be Element of ( Domains_of Y) st a = A & b = B holds (a "\/" b) = (A \/ B) & (a "/\" b) = (A /\ B)

    proof

      let a,b be Element of ( Domains_Lattice Y);

      let A,B be Element of ( Domains_of Y);

      assume that

       A1: a = A and

       A2: b = B;



      thus (a "\/" b) = (( D-Union Y) . (A,B)) by A1, A2, LATTICES:def 1

      .= (A \/ B) by Th45;



      thus (a "/\" b) = (( D-Meet Y) . (A,B)) by A1, A2, LATTICES:def 2

      .= (A /\ B) by Th45;

    end;

    theorem :: TDLAT_3:47

    for F be Subset-Family of Y st F is domains-family holds for S be Subset of ( Domains_Lattice Y) st S = F holds ( "\/" (S,( Domains_Lattice Y))) = ( Cl ( union F))

    proof

      let F be Subset-Family of Y;

      assume F is domains-family;

      then F c= ( Domains_of Y) by TDLAT_2: 65;

      then F c= ( Closed_Domains_of Y) by Th39;

      then

       A1: F is closed-domains-family by TDLAT_2: 72;

      let S be Subset of ( Domains_Lattice Y);

      reconsider P = S as Subset of ( Closed_Domains_Lattice Y) by Th41;

      assume

       A2: S = F;



      thus ( "\/" (S,( Domains_Lattice Y))) = ( "\/" (P,( Closed_Domains_Lattice Y))) by Th41

      .= ( Cl ( union F)) by A1, A2, TDLAT_2: 100;

    end;

    theorem :: TDLAT_3:48

    for F be Subset-Family of Y st F is domains-family holds for S be Subset of ( Domains_Lattice Y) st S = F holds (S <> {} implies ( "/\" (S,( Domains_Lattice Y))) = ( Int ( meet F))) & (S = {} implies ( "/\" (S,( Domains_Lattice Y))) = ( [#] Y))

    proof

      let F be Subset-Family of Y;

      assume

       A1: F is domains-family;

      then F c= ( Domains_of Y) by TDLAT_2: 65;

      then F c= ( Open_Domains_of Y) by Th42;

      then

       A2: F is open-domains-family by TDLAT_2: 79;

      let S be Subset of ( Domains_Lattice Y);

      assume

       A3: S = F;

      ( Domains_Lattice Y) = ( Open_Domains_Lattice Y) by Th44;

      hence S <> {} implies ( "/\" (S,( Domains_Lattice Y))) = ( Int ( meet F)) by A2, A3, TDLAT_2: 110;

      assume S = {} ;

      hence thesis by A1, A3, TDLAT_2: 93;

    end;

    reserve X for non empty TopSpace;

    theorem :: TDLAT_3:49



     Th49: X is extremally_disconnected iff ( Domains_Lattice X) is M_Lattice

    proof

      thus X is extremally_disconnected implies ( Domains_Lattice X) is M_Lattice

      proof

        assume X is extremally_disconnected;

        then ( Domains_Lattice X) = ( Open_Domains_Lattice X) by Th44;

        hence thesis;

      end;

      assume

       A1: ( Domains_Lattice X) is M_Lattice;

      assume not X is extremally_disconnected;

      then

      consider D be Subset of X such that

       A2: D is condensed and

       A3: ( Int ( Cl D)) <> ( Cl ( Int D)) by Th34;

      set A = ( Int ( Cl D)), C = ( Cl ( Int D)), B = (C ` );



       A4: D c= C by A2, TOPS_1:def 6;

      A c= D by A2, TOPS_1:def 6;

      then

       A5: A c= C by A4;



       A6: A is open_condensed by TDLAT_1: 23;

      then

       A7: A = ( Int ( Cl A)) by TOPS_1:def 8;

      B misses C by XBOOLE_1: 79;

      then

       A8: (B /\ C) = ( {} X);



       A9: C is closed_condensed by TDLAT_1: 22;

      then

       A10: C = ( Cl ( Int C)) by TOPS_1:def 7;

      C is condensed by A9, TOPS_1: 66;

      then

       A11: C in { E where E be Subset of X : E is condensed };

      reconsider c = C as Element of ( Domains_Lattice X) by A11;

      A is condensed by A6, TOPS_1: 67;

      then A in { E where E be Subset of X : E is condensed };

      then

      reconsider a = A as Element of ( Domains_Lattice X);



       A15: B = ( Int (( Int D) ` )) by Th3

      .= ( Int ( Cl (D ` ))) by Th2;

      (B ` ) is closed_condensed by TDLAT_1: 22;

      then B is open_condensed by TOPS_1: 61;

      then B is condensed by TOPS_1: 67;

      then B in { E where E be Subset of X : E is condensed };

      then

      reconsider b = B as Element of ( Domains_Lattice X);



       A16: (A \/ ( {} X)) = A;

      ( Cl (A \/ B)) = (( Cl A) \/ ( Cl B)) by PRE_TOPC: 20

      .= ( Cl ( Int (( Cl D) \/ ( Cl (D ` ))))) by A15, TDLAT_1: 6

      .= ( Cl ( Int ( Cl (D \/ (D ` ))))) by PRE_TOPC: 20

      .= ( Cl ( Int ( Cl ( [#] X)))) by PRE_TOPC: 2

      .= ( Cl ( Int ( [#] X))) by TOPS_1: 2

      .= ( Cl ( [#] X)) by TOPS_1: 15

      .= ( [#] X) by TOPS_1: 2;



      then (a "\/" b) = (( Int ( [#] X)) \/ (A \/ B)) by TDLAT_2: 87

      .= (( [#] X) \/ (A \/ B)) by TOPS_1: 15

      .= ( [#] X) by XBOOLE_1: 12;



      then

       A17: ((a "\/" b) "/\" c) = (( Cl ( Int (( [#] X) /\ C))) /\ (( [#] X) /\ C)) by TDLAT_2: 87

      .= (( Cl ( Int C)) /\ (( [#] X) /\ C)) by XBOOLE_1: 28

      .= (( Cl ( Int C)) /\ C) by XBOOLE_1: 28

      .= C by A10;



       A18: a [= c by A5, TDLAT_2: 89;

      (b "/\" c) = (( Cl ( Int (B /\ C))) /\ (B /\ C)) by TDLAT_2: 87

      .= ( {} X) by A8;



      then (a "\/" (b "/\" c)) = (( Int ( Cl A)) \/ A) by A16, TDLAT_2: 87

      .= A by A7;

      hence contradiction by A1, A3, A18, A17, LATTICES:def 12;

    end;

    theorem :: TDLAT_3:50

    ( Domains_Lattice X) = ( Closed_Domains_Lattice X) implies X is extremally_disconnected by Th49;

    theorem :: TDLAT_3:51

    ( Domains_Lattice X) = ( Open_Domains_Lattice X) implies X is extremally_disconnected by Th49;

    theorem :: TDLAT_3:52

    ( Closed_Domains_Lattice X) = ( Open_Domains_Lattice X) implies X is extremally_disconnected

    proof

      assume ( Closed_Domains_Lattice X) = ( Open_Domains_Lattice X);

      then

       A1: ( Closed_Domains_of X) = ( Open_Domains_of X);

      for A be Subset of X holds (A is open_condensed implies A is closed_condensed) & (A is closed_condensed implies A is open_condensed)

      proof

        let A be Subset of X;

        thus A is open_condensed implies A is closed_condensed

        proof

          assume A is open_condensed;

          then A in { E where E be Subset of X : E is open_condensed };

          then A in ( Closed_Domains_of X) by A1;

          then A in { E where E be Subset of X : E is closed_condensed };

          then ex D be Subset of X st D = A & D is closed_condensed;

          hence thesis;

        end;

        assume A is closed_condensed;

        then A in { E where E be Subset of X : E is closed_condensed };

        then A in ( Open_Domains_of X) by A1;

        then A in { E where E be Subset of X : E is open_condensed };

        then ex D be Subset of X st D = A & D is open_condensed;

        hence thesis;

      end;

      hence thesis by Th36;

    end;

    theorem :: TDLAT_3:53

    X is extremally_disconnected iff ( Domains_Lattice X) is B_Lattice

    proof

      thus X is extremally_disconnected implies ( Domains_Lattice X) is B_Lattice

      proof

        assume X is extremally_disconnected;

        then ( Domains_Lattice X) = ( Open_Domains_Lattice X) by Th44;

        hence thesis;

      end;

      assume ( Domains_Lattice X) is B_Lattice;

      hence thesis by Th49;

    end;