tdlat_2.miz



    begin

    reserve T for TopSpace;

    theorem :: TDLAT_2:1

    

     Th1: for A be Subset of T holds ( Int ( Cl ( Int A))) c= ( Int ( Cl A)) & ( Int ( Cl ( Int A))) c= ( Cl ( Int A))

    proof

      let A be Subset of T;

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

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

      thus thesis by TOPS_1: 16;

    end;

    theorem :: TDLAT_2:2

    

     Th2: for A be Subset of T holds ( Cl ( Int A)) c= ( Cl ( Int ( Cl A))) & ( Int ( Cl A)) c= ( Cl ( Int ( Cl A)))

    proof

      let A be Subset of T;

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

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

      thus thesis by PRE_TOPC: 18;

    end;

    theorem :: TDLAT_2:3

    for A,B be Subset of T st B is closed holds ( Cl ( Int (A /\ B))) = A implies A c= B

    proof

      let A,B be Subset of T;

      assume

       A1: B is closed;

      

       A2: (A /\ B) c= B by XBOOLE_1: 17;

      ( Int (A /\ B)) c= (A /\ B) by TOPS_1: 16;

      then ( Int (A /\ B)) c= B by A2;

      then

       A3: ( Cl ( Int (A /\ B))) c= ( Cl B) by PRE_TOPC: 19;

      assume ( Cl ( Int (A /\ B))) = A;

      hence thesis by A1, A3, PRE_TOPC: 22;

    end;

    theorem :: TDLAT_2:4

    

     Th4: for A,B be Subset of T st A is open holds ( Int ( Cl (A \/ B))) = B implies A c= B

    proof

      let A,B be Subset of T;

      assume

       A1: A is open;

      

       A2: A c= (A \/ B) by XBOOLE_1: 7;

      (A \/ B) c= ( Cl (A \/ B)) by PRE_TOPC: 18;

      then A c= ( Cl (A \/ B)) by A2;

      then

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

      assume ( Int ( Cl (A \/ B))) = B;

      hence thesis by A1, A3, TOPS_1: 23;

    end;

    theorem :: TDLAT_2:5

    

     Th5: for A be Subset of T st A c= ( Cl ( Int A)) holds (A \/ ( Int ( Cl A))) c= ( Cl ( Int (A \/ ( Int ( Cl A)))))

    proof

      let A be Subset of T;

      assume

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

      

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

      

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

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

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

      then (A \/ ( Int ( Cl A))) c= (( Cl ( Int ( Cl A))) \/ ( Cl ( Int ( Cl A)))) by A2, XBOOLE_1: 13;

      then

       A4: (A \/ ( Int ( Cl A))) c= ( Cl (( Int A) \/ ( Int ( Cl A)))) by A3, XBOOLE_1: 12;

      (( Int A) \/ ( Int ( Int ( Cl A)))) c= ( Int (A \/ ( Int ( Cl A)))) by TOPS_1: 20;

      then ( Cl (( Int A) \/ ( Int ( Cl A)))) c= ( Cl ( Int (A \/ ( Int ( Cl A))))) by PRE_TOPC: 19;

      hence thesis by A4;

    end;

    theorem :: TDLAT_2:6

    

     Th6: for A be Subset of T st ( Int ( Cl A)) c= A holds ( Int ( Cl (A /\ ( Cl ( Int A))))) c= (A /\ ( Cl ( Int A)))

    proof

      let A be Subset of T;

      assume

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

      

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

      

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

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

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

      then (( Int ( Cl ( Int A))) /\ ( Int ( Cl ( Int A)))) c= (A /\ ( Cl ( Int A))) by A2, XBOOLE_1: 27;

      then

       A4: ( Int (( Cl A) /\ ( Cl ( Int A)))) c= (A /\ ( Cl ( Int A))) by A3, XBOOLE_1: 28;

      ( Cl (A /\ ( Cl ( Int A)))) c= (( Cl A) /\ ( Cl ( Cl ( Int A)))) by PRE_TOPC: 21;

      then ( Int ( Cl (A /\ ( Cl ( Int A))))) c= ( Int (( Cl A) /\ ( Cl ( Int A)))) by TOPS_1: 19;

      hence thesis by A4;

    end;

    begin

    notation

      let T;

      let F be Subset-Family of T;

      synonym Cl F for clf F;

    end

    theorem :: TDLAT_2:7

    

     Th7: for F be Subset-Family of T holds ( Cl F) = { A where A be Subset of T : ex B be Subset of T st A = ( Cl B) & B in F }

    proof

      let F be Subset-Family of T;

      set P = { A where A be Subset of T : ex B be Subset of T st A = ( Cl B) & B in F };

      now

        let C be object;

        assume C in P;

        then ex A be Subset of T st C = A & ex B be Subset of T st A = ( Cl B) & B in F;

        hence C in ( bool the carrier of T);

      end;

      then

      reconsider P as Subset-Family of T by TARSKI:def 3;

      reconsider P as Subset-Family of T;

      for X be object holds X in ( Cl F) iff X in P

      proof

        let X be object;

         A1:

        now

          assume

           A2: X in P;

          then

          reconsider C = X as Subset of T;

          ex D be Subset of T st D = C & ex B be Subset of T st D = ( Cl B) & B in F by A2;

          hence X in ( Cl F) by PCOMPS_1:def 2;

        end;

        now

          assume

           A3: X in ( Cl F);

          then

          reconsider C = X as Subset of T;

          ex B be Subset of T st C = ( Cl B) & B in F by A3, PCOMPS_1:def 2;

          hence X in P;

        end;

        hence thesis by A1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:8

    for F be Subset-Family of T holds ( Cl F) = ( Cl ( Cl F))

    proof

      let F be Subset-Family of T;

      

       A1: ( Cl ( Cl F)) = { D where D be Subset of T : ex B be Subset of T st D = ( Cl B) & B in ( Cl F) } by Th7;

      

       A2: ( Cl F) = { A where A be Subset of T : ex B be Subset of T st A = ( Cl B) & B in F } by Th7;

      for X be object holds X in ( Cl F) iff X in ( Cl ( Cl F))

      proof

        let X be object;

         A3:

        now

          assume

           A4: X in ( Cl F);

          then

          reconsider C = X as Subset of T;

          consider B be Subset of T such that

           A5: C = ( Cl B) and

           A6: B in F by A4, PCOMPS_1:def 2;

          

           A7: ( Cl B) in ( Cl F) by A6, PCOMPS_1:def 2;

          C = ( Cl ( Cl B)) by A5;

          hence X in ( Cl ( Cl F)) by A1, A7;

        end;

        now

          assume

           A8: X in ( Cl ( Cl F));

          then

          reconsider C = X as Subset of T;

          ex Q be Subset of T st Q = C & ex B be Subset of T st Q = ( Cl B) & B in ( Cl F) by A1, A8;

          then

          consider B be Subset of T such that

           A9: C = ( Cl B) and

           A10: B in ( Cl F);

          ex Q be Subset of T st Q = B & ex R be Subset of T st Q = ( Cl R) & R in F by A2, A10;

          hence X in ( Cl F) by A9, PCOMPS_1:def 2;

        end;

        hence thesis by A3;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:9

    

     Th9: for F be Subset-Family of T holds F = {} iff ( Cl F) = {}

    proof

      let F be Subset-Family of T;

      thus F = {} implies ( Cl F) = {} by PCOMPS_1: 12;

      assume

       A1: ( Cl F) = {} ;

      set B = the Element of F;

      assume

       A2: F <> {} ;

      then

      reconsider B as Subset of T by TARSKI:def 3;

      ( Cl B) in ( Cl F) by A2, PCOMPS_1:def 2;

      hence contradiction by A1;

    end;

    theorem :: TDLAT_2:10

    for F,G be Subset-Family of T holds ( Cl (F /\ G)) c= (( Cl F) /\ ( Cl G))

    proof

      let F,G be Subset-Family of T;

      for X be object holds X in ( Cl (F /\ G)) implies X in (( Cl F) /\ ( Cl G))

      proof

        let X be object;

        assume

         A1: X in ( Cl (F /\ G));

        then

        reconsider X0 = X as Subset of T;

        consider W be Subset of T such that

         A2: X0 = ( Cl W) and

         A3: W in (F /\ G) by A1, PCOMPS_1:def 2;

        W in G by A3, XBOOLE_0:def 4;

        then

         A4: X0 in ( Cl G) by A2, PCOMPS_1:def 2;

        W in F by A3, XBOOLE_0:def 4;

        then X0 in ( Cl F) by A2, PCOMPS_1:def 2;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:11

    for F,G be Subset-Family of T holds (( Cl F) \ ( Cl G)) c= ( Cl (F \ G))

    proof

      let F,G be Subset-Family of T;

      for X be object holds X in (( Cl F) \ ( Cl G)) implies X in ( Cl (F \ G))

      proof

        let X be object;

        assume

         A1: X in (( Cl F) \ ( Cl G));

        then

        reconsider X0 = X as Subset of T;

        X in ( Cl F) by A1, XBOOLE_0:def 5;

        then

        consider W be Subset of T such that

         A2: X0 = ( Cl W) and

         A3: W in F by PCOMPS_1:def 2;

         not X in ( Cl G) by A1, XBOOLE_0:def 5;

        then not W in G by A2, PCOMPS_1:def 2;

        then W in (F \ G) by A3, XBOOLE_0:def 5;

        hence thesis by A2, PCOMPS_1:def 2;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:12

    for F be Subset-Family of T, A be Subset of T st A in F holds ( meet ( Cl F)) c= ( Cl A) & ( Cl A) c= ( union ( Cl F))

    proof

      let F be Subset-Family of T, A be Subset of T;

      assume A in F;

      then ( Cl A) in { P where P be Subset of T : ex B be Subset of T st P = ( Cl B) & B in F };

      then

       A1: ( Cl A) in ( Cl F) by Th7;

      hence ( meet ( Cl F)) c= ( Cl A) by SETFAM_1: 3;

      thus thesis by A1, ZFMISC_1: 74;

    end;

    theorem :: TDLAT_2:13

    

     Th13: for F be Subset-Family of T holds ( meet F) c= ( meet ( Cl F))

    proof

      let F be Subset-Family of T;

      

       A1: for A be set st A in ( Cl F) holds ( meet F) c= A

      proof

        let A be set;

        assume

         A2: A in ( Cl F);

        then

        reconsider A0 = A as Subset of T;

        consider B be Subset of T such that

         A3: A0 = ( Cl B) and

         A4: B in F by A2, PCOMPS_1:def 2;

        

         A5: B c= A0 by A3, PRE_TOPC: 18;

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

        hence thesis by A5;

      end;

      now

        per cases ;

          suppose ( Cl F) = {} ;

          hence thesis by Th9;

        end;

          suppose ( Cl F) <> {} ;

          hence thesis by A1, SETFAM_1: 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:14

    

     Th14: for F be Subset-Family of T holds ( Cl ( meet F)) c= ( meet ( Cl F))

    proof

      let F be Subset-Family of T;

      

       A1: ( meet ( Cl F)) is closed by PCOMPS_1: 11, TOPS_2: 22;

      ( Cl ( meet F)) c= ( Cl ( meet ( Cl F))) by Th13, PRE_TOPC: 19;

      hence thesis by A1, PRE_TOPC: 22;

    end;

    theorem :: TDLAT_2:15

    

     Th15: for F be Subset-Family of T holds ( union ( Cl F)) c= ( Cl ( union F))

    proof

      let F be Subset-Family of T;

      for A be set st A in ( Cl F) holds A c= ( Cl ( union F))

      proof

        let A be set;

        assume

         A1: A in ( Cl F);

        then

        reconsider A0 = A as Subset of T;

        ex B be Subset of T st A0 = ( Cl B) & B in F by A1, PCOMPS_1:def 2;

        hence thesis by PRE_TOPC: 19, ZFMISC_1: 74;

      end;

      hence thesis by ZFMISC_1: 76;

    end;

    definition

      let T;

      let F be Subset-Family of T;

      :: TDLAT_2:def1

      func Int F -> Subset-Family of T means

      : Def1: for A be Subset of T holds A in it iff ex B be Subset of T st A = ( Int B) & B in F;

      existence

      proof

        defpred X[ Subset of T] means ex B be Subset of T st $1 = ( Int B) & B in F;

        thus ex F be Subset-Family of T st for A be Subset of T holds A in F iff X[A] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        let H,G be Subset-Family of T;

        assume

         A1: for A be Subset of T holds A in H iff ex B be Subset of T st A = ( Int B) & B in F;

        assume

         A2: for A be Subset of T holds A in G iff ex B be Subset of T st A = ( Int B) & B in F;

        now

          let A be object;

          assume

           A3: A in G;

          then

          reconsider A0 = A as Subset of T;

          ex B be Subset of T st A0 = ( Int B) & B in F by A2, A3;

          hence A in H by A1;

        end;

        then

         A4: G c= H;

        now

          let A be object;

          assume

           A5: A in H;

          then

          reconsider A0 = A as Subset of T;

          ex B be Subset of T st A0 = ( Int B) & B in F by A1, A5;

          hence A in G by A2;

        end;

        then H c= G;

        hence thesis by A4, XBOOLE_0:def 10;

      end;

      projectivity

      proof

        let G,F be Subset-Family of T such that

         A6: for A be Subset of T holds A in G iff ex B be Subset of T st A = ( Int B) & B in F;

        let A be Subset of T;

        thus A in G implies ex B be Subset of T st A = ( Int B) & B in G

        proof

          assume A in G;

          then

          consider B be Subset of T such that

           A7: A = ( Int B) and

           A8: B in F by A6;

          take C = ( Int B);

          thus A = ( Int C) by A7;

          thus C in G by A8, A6;

        end;

        given B be Subset of T such that

         A9: A = ( Int B) and

         A10: B in G;

        consider C be Subset of T such that

         A11: B = ( Int C) and C in F by A10, A6;

        A = B by A9, A11;

        hence A in G by A10;

      end;

    end

    theorem :: TDLAT_2:16

    

     Th16: for F be Subset-Family of T holds ( Int F) = { A where A be Subset of T : ex B be Subset of T st A = ( Int B) & B in F }

    proof

      let F be Subset-Family of T;

      set P = { A where A be Subset of T : ex B be Subset of T st A = ( Int B) & B in F };

      now

        let C be object;

        assume C in P;

        then ex A be Subset of T st C = A & ex B be Subset of T st A = ( Int B) & B in F;

        hence C in ( bool the carrier of T);

      end;

      then

      reconsider P as Subset-Family of T by TARSKI:def 3;

      reconsider P as Subset-Family of T;

      for X be object holds X in ( Int F) iff X in P

      proof

        let X be object;

         A1:

        now

          assume

           A2: X in P;

          then

          reconsider C = X as Subset of T;

          ex D be Subset of T st D = C & ex B be Subset of T st D = ( Int B) & B in F by A2;

          hence X in ( Int F) by Def1;

        end;

        now

          assume

           A3: X in ( Int F);

          then

          reconsider C = X as Subset of T;

          ex B be Subset of T st C = ( Int B) & B in F by A3, Def1;

          hence X in P;

        end;

        hence thesis by A1;

      end;

      hence thesis by TARSKI: 2;

    end;

    ::$Canceled

    theorem :: TDLAT_2:18

    

     Th17: for F be Subset-Family of T holds ( Int F) is open

    proof

      let F be Subset-Family of T;

      now

        let A be Subset of T;

        assume A in ( Int F);

        then ex B be Subset of T st A = ( Int B) & B in F by Def1;

        hence A is open;

      end;

      hence thesis by TOPS_2:def 1;

    end;

    theorem :: TDLAT_2:19

    

     Th18: for F be Subset-Family of T holds F = {} iff ( Int F) = {}

    proof

      let F be Subset-Family of T;

      thus F = {} implies ( Int F) = {}

      proof

        set A = the Element of ( Int F);

        assume

         A1: F = {} ;

        assume

         A2: not thesis;

        then

        reconsider A as Subset of T by TARSKI:def 3;

        ex V be Subset of T st A = ( Int V) & V in F by A2, Def1;

        hence contradiction by A1;

      end;

      thus ( Int F) = {} implies F = {}

      proof

        set B = the Element of F;

        assume

         A3: ( Int F) = {} ;

        assume

         A4: not thesis;

        then

        reconsider B as Subset of T by TARSKI:def 3;

        reconsider A = ( Int B) as set;

        ex A be set st A in ( Int F)

        proof

          take A;

          thus thesis by A4, Def1;

        end;

        hence contradiction by A3;

      end;

    end;

    theorem :: TDLAT_2:20

    

     Th19: for A be Subset of T, F be Subset-Family of T st F = {A} holds ( Int F) = {( Int A)}

    proof

      let A be Subset of T, F be Subset-Family of T;

      reconsider C = ( Int F) as set;

      assume

       A1: F = {A};

      for B be object holds B in C iff B = ( Int A)

      proof

        let B be object;

         A2:

        now

          assume

           A3: B = ( Int A);

          ex M be Subset of T st B = ( Int M) & M in F

          proof

            take A;

            thus thesis by A1, A3, TARSKI:def 1;

          end;

          hence B in C by Def1;

        end;

        now

          assume

           A4: B in C;

          then

          reconsider B0 = B as Subset of T;

          ex M be Subset of T st B0 = ( Int M) & M in F by A4, Def1;

          hence B = ( Int A) by A1, TARSKI:def 1;

        end;

        hence thesis by A2;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: TDLAT_2:21

    for F,G be Subset-Family of T holds F c= G implies ( Int F) c= ( Int G)

    proof

      let F,G be Subset-Family of T;

      reconsider F0 = ( Int F), G0 = ( Int G) as set;

      assume

       A1: F c= G;

      now

        let X be object;

        assume

         A2: X in F0;

        then

        reconsider X0 = X as Subset of T;

        ex V be Subset of T st X0 = ( Int V) & V in F by A2, Def1;

        hence X in G0 by A1, Def1;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:22

    

     Th21: for F,G be Subset-Family of T holds ( Int (F \/ G)) = (( Int F) \/ ( Int G))

    proof

      let F,G be Subset-Family of T;

      for X be object holds X in ( Int (F \/ G)) iff X in (( Int F) \/ ( Int G))

      proof

        let X be object;

         A1:

        now

          assume

           A2: X in (( Int F) \/ ( Int G));

          now

            per cases by A2, XBOOLE_0:def 3;

              suppose

               A3: X in ( Int F);

              then

              reconsider X0 = X as Subset of T;

              ex W be Subset of T st X0 = ( Int W) & W in (F \/ G)

              proof

                consider Z be Subset of T such that

                 A4: X0 = ( Int Z) and

                 A5: Z in F by A3, Def1;

                take Z;

                thus thesis by A4, A5, XBOOLE_0:def 3;

              end;

              hence X in ( Int (F \/ G)) by Def1;

            end;

              suppose

               A6: X in ( Int G);

              then

              reconsider X0 = X as Subset of T;

              ex W be Subset of T st X0 = ( Int W) & W in (F \/ G)

              proof

                consider Z be Subset of T such that

                 A7: X0 = ( Int Z) and

                 A8: Z in G by A6, Def1;

                take Z;

                thus thesis by A7, A8, XBOOLE_0:def 3;

              end;

              hence X in ( Int (F \/ G)) by Def1;

            end;

          end;

          hence X in ( Int (F \/ G));

        end;

        now

          assume

           A9: X in ( Int (F \/ G));

          then

          reconsider X0 = X as Subset of T;

          consider W be Subset of T such that

           A10: X0 = ( Int W) and

           A11: W in (F \/ G) by A9, Def1;

          now

            per cases by A11, XBOOLE_0:def 3;

              suppose W in F;

              then X0 in ( Int F) by A10, Def1;

              hence X0 in (( Int F) \/ ( Int G)) by XBOOLE_0:def 3;

            end;

              suppose W in G;

              then X0 in ( Int G) by A10, Def1;

              hence X0 in (( Int F) \/ ( Int G)) by XBOOLE_0:def 3;

            end;

          end;

          hence X in (( Int F) \/ ( Int G));

        end;

        hence thesis by A1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:23

    for F,G be Subset-Family of T holds ( Int (F /\ G)) c= (( Int F) /\ ( Int G))

    proof

      let F,G be Subset-Family of T;

      for X be object holds X in ( Int (F /\ G)) implies X in (( Int F) /\ ( Int G))

      proof

        let X be object;

        assume

         A1: X in ( Int (F /\ G));

        then

        reconsider X0 = X as Subset of T;

        consider W be Subset of T such that

         A2: X0 = ( Int W) and

         A3: W in (F /\ G) by A1, Def1;

        W in G by A3, XBOOLE_0:def 4;

        then

         A4: X0 in ( Int G) by A2, Def1;

        W in F by A3, XBOOLE_0:def 4;

        then X0 in ( Int F) by A2, Def1;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:24

    for F,G be Subset-Family of T holds (( Int F) \ ( Int G)) c= ( Int (F \ G))

    proof

      let F,G be Subset-Family of T;

      for X be object holds X in (( Int F) \ ( Int G)) implies X in ( Int (F \ G))

      proof

        let X be object;

        assume

         A1: X in (( Int F) \ ( Int G));

        then

        reconsider X0 = X as Subset of T;

        X in ( Int F) by A1, XBOOLE_0:def 5;

        then

        consider W be Subset of T such that

         A2: X0 = ( Int W) and

         A3: W in F by Def1;

         not X in ( Int G) by A1, XBOOLE_0:def 5;

        then not W in G by A2, Def1;

        then W in (F \ G) by A3, XBOOLE_0:def 5;

        hence thesis by A2, Def1;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:25

    for F be Subset-Family of T, A be Subset of T holds A in F implies ( Int A) c= ( union ( Int F)) & ( meet ( Int F)) c= ( Int A)

    proof

      let F be Subset-Family of T, A be Subset of T;

      assume A in F;

      then ( Int A) in { P where P be Subset of T : ex B be Subset of T st P = ( Int B) & B in F };

      then

       A1: ( Int A) in ( Int F) by Th16;

      hence ( Int A) c= ( union ( Int F)) by ZFMISC_1: 74;

      thus thesis by A1, SETFAM_1: 3;

    end;

    theorem :: TDLAT_2:26

    

     Th25: for F be Subset-Family of T holds ( union ( Int F)) c= ( union F)

    proof

      let F be Subset-Family of T;

      now

        let x be object;

        assume x in ( union ( Int F));

        then

        consider A be set such that

         A1: x in A and

         A2: A in ( Int F) by TARSKI:def 4;

        reconsider A as Subset of T by A2;

        consider B be Subset of T such that

         A3: A = ( Int B) and

         A4: B in F by A2, Def1;

        ex B be set st x in B & B in F

        proof

          take B;

          ( Int B) c= B by TOPS_1: 16;

          hence thesis by A1, A3, A4;

        end;

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

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:27

    for F be Subset-Family of T holds ( meet ( Int F)) c= ( meet F)

    proof

      let F be Subset-Family of T;

      

       A1: for A be set st A in F holds ( meet ( Int F)) c= A

      proof

        let A be set;

        assume

         A2: A in F;

        then

        reconsider A0 = A as Subset of T;

        set C = ( Int A0);

        C in { P where P be Subset of T : ex Q be Subset of T st P = ( Int Q) & Q in F } by A2;

        then C in ( Int F) by Th16;

        then

         A3: ( meet ( Int F)) c= C by SETFAM_1: 3;

        C c= A0 by TOPS_1: 16;

        hence thesis by A3;

      end;

      now

        per cases ;

          suppose F = {} ;

          hence thesis by Th18;

        end;

          suppose F <> {} ;

          hence thesis by A1, SETFAM_1: 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:28

    

     Th27: for F be Subset-Family of T holds ( union ( Int F)) c= ( Int ( union F))

    proof

      let F be Subset-Family of T;

      

       A1: ( Int ( union ( Int F))) c= ( Int ( union F)) by Th25, TOPS_1: 19;

      ( union ( Int F)) is open by Th17, TOPS_2: 19;

      hence thesis by A1, TOPS_1: 23;

    end;

    theorem :: TDLAT_2:29

    

     Th28: for F be Subset-Family of T holds ( Int ( meet F)) c= ( meet ( Int F))

    proof

      let F be Subset-Family of T;

      

       A1: for A be set st A in ( Int F) holds ( Int ( meet F)) c= A

      proof

        let A be set;

        assume

         A2: A in ( Int F);

        then

        reconsider A0 = A as Subset of T;

        A0 in { B where B be Subset of T : ex C be Subset of T st B = ( Int C) & C in F } by A2, Th16;

        then ex P be Subset of T st P = A0 & ex C be Subset of T st P = ( Int C) & C in F;

        hence thesis by SETFAM_1: 3, TOPS_1: 19;

      end;

      now

        per cases ;

          suppose ( Int F) = {} ;

          then ( meet F) = ( {} T) by Th18, SETFAM_1: 1;

          hence thesis;

        end;

          suppose ( Int F) <> {} ;

          hence thesis by A1, SETFAM_1: 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:30

    for F be Subset-Family of T holds F is finite implies ( Int ( meet F)) = ( meet ( Int F))

    proof

      let F be Subset-Family of T;

      assume

       A1: F is finite;

      

       A2: ( meet ( Int F)) c= ( Int ( meet F))

      proof

        consider p be FinSequence such that

         A3: ( rng p) = F by A1, FINSEQ_1: 52;

        consider n be Nat such that

         A4: ( dom p) = ( Seg n) by FINSEQ_1:def 2;

        defpred X[ Nat] means for G be Subset-Family of T st G = (p .: ( Seg $1)) & $1 <= n & 1 <= n holds ( meet ( Int G)) c= ( Int ( meet G));

        

         A5: for k be Nat st X[k] holds X[(k + 1)]

        proof

          let k be Nat;

          assume

           A6: for G be Subset-Family of T st G = (p .: ( Seg k)) & k <= n & 1 <= n holds ( meet ( Int G)) c= ( Int ( meet G));

          let G be Subset-Family of T;

          assume

           A7: G = (p .: ( Seg (k + 1)));

          assume that

           A8: (k + 1) <= n and

           A9: 1 <= n;

           A10:

          now

            reconsider G2 = ( Im (p,(k + 1))) as Subset-Family of T by A3, RELAT_1: 111, TOPS_2: 2;

            reconsider G1 = (p .: ( Seg k)) as Subset-Family of T by A3, RELAT_1: 111, TOPS_2: 2;

            

             A11: ( 0 + 1) = 1;

             0 <= k by NAT_1: 2;

            then 1 <= (k + 1) by A11, XREAL_1: 7;

            then

             A12: (k + 1) in ( dom p) by A4, A8, FINSEQ_1: 1;

            then

             A13: G2 = {(p . (k + 1))} by FUNCT_1: 59;

            then ( meet G2) = (p . (k + 1)) by SETFAM_1: 10;

            then

            reconsider G3 = (p . (k + 1)) as Subset of T;

            

             A14: ( meet ( Int G2)) = ( meet {( Int G3)}) by A13, Th19

            .= ( Int G3) by SETFAM_1: 10

            .= ( Int ( meet G2)) by A13, SETFAM_1: 10;

            (k + 1) <= (n + 1) by A8, NAT_1: 12;

            then k <= n by XREAL_1: 6;

            then

             A15: ( meet ( Int G1)) c= ( Int ( meet G1)) by A6, A9;

            assume 0 < k;

            then

             A16: ( 0 + 1) <= k by NAT_1: 13;

            then

             A17: k in ( Seg k) by FINSEQ_1: 1;

            k <= n by A8, NAT_1: 13;

            then k in ( dom p) by A4, A16, FINSEQ_1: 1;

            then

             A18: (p . k) in G1 by A17, FUNCT_1:def 6;

            (k + 1) in {(k + 1)} by TARSKI:def 1;

            then

             A19: (p . (k + 1)) in G2 by A12, FUNCT_1:def 6;

            then

             A20: ( Int G2) <> {} by Th18;

            

             A21: (p .: ( Seg (k + 1))) = (p .: (( Seg k) \/ {(k + 1)})) by FINSEQ_1: 9

            .= ((p .: ( Seg k)) \/ (p .: {(k + 1)})) by RELAT_1: 120;

            

            then ( Int ( meet G)) = ( Int (( meet G1) /\ ( meet G2))) by A7, A18, A19, SETFAM_1: 9

            .= (( Int ( meet G1)) /\ ( Int ( meet G2))) by TOPS_1: 17;

            then

             A22: (( meet ( Int G1)) /\ ( meet ( Int G2))) c= ( Int ( meet G)) by A14, A15, XBOOLE_1: 27;

            ( Int G1) <> {} by A18, Th18;

            then ( meet (( Int G1) \/ ( Int G2))) c= ( Int ( meet G)) by A20, A22, SETFAM_1: 9;

            hence thesis by A7, A21, Th21;

          end;

          now

            assume

             A23: k = 0 ;

            then 1 in ( dom p) by A4, A8, FINSEQ_1: 1;

            then

             A24: ( Im (p,1)) = {(p . 1)} by FUNCT_1: 59;

            then ( union G) = (p . 1) by A7, A23, FINSEQ_1: 2, ZFMISC_1: 25;

            then

            reconsider G1 = (p . 1) as Subset of T;

            ( Int ( meet G)) = ( Int G1) by A7, A23, A24, FINSEQ_1: 2, SETFAM_1: 10

            .= ( meet {( Int G1)}) by SETFAM_1: 10

            .= ( meet ( Int G)) by A7, A23, A24, Th19, FINSEQ_1: 2;

            hence thesis;

          end;

          hence thesis by A10, NAT_1: 3;

        end;

        

         A25: X[ 0 ] by Th18, SETFAM_1: 1;

        

         A26: for k be Nat holds X[k] from NAT_1:sch 2( A25, A5);

         A27:

        now

          assume

           A28: 1 <= n;

          F = (p .: ( Seg n)) by A3, A4, RELAT_1: 113;

          hence thesis by A26, A28;

        end;

         A29:

        now

          assume n <> 0 ;

          then

           A30: 0 < n by NAT_1: 3;

          1 = ( 0 + 1);

          hence 1 <= n by A30, NAT_1: 13;

        end;

        now

          assume n = 0 ;

          then ( Seg n) = {} ;

          then F = (p .: {} ) by A3, A4, RELAT_1: 113;

          then F = {} ;

          hence thesis by Th18, SETFAM_1: 1;

        end;

        hence thesis by A27, A29;

      end;

      ( Int ( meet F)) c= ( meet ( Int F)) by Th28;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    reserve T for non empty TopSpace;

    reserve F for Subset-Family of T;

    theorem :: TDLAT_2:31

    

     Th30: ( Cl ( Int F)) = { A where A be Subset of T : ex B be Subset of T st A = ( Cl ( Int B)) & B in F }

    proof

      set P = { A where A be Subset of T : ex B be Subset of T st A = ( Cl ( Int B)) & B in F };

      now

        let C be object;

        assume C in P;

        then ex A be Subset of T st C = A & ex B be Subset of T st A = ( Cl ( Int B)) & B in F;

        hence C in ( bool the carrier of T);

      end;

      then

      reconsider P as Subset-Family of T by TARSKI:def 3;

      reconsider P as Subset-Family of T;

      for X be object holds X in ( Cl ( Int F)) iff X in P

      proof

        let X be object;

         A1:

        now

          assume

           A2: X in P;

          then

          reconsider C = X as Subset of T;

          ex D be Subset of T st D = C & ex B be Subset of T st D = ( Cl ( Int B)) & B in F by A2;

          then

          consider B be Subset of T such that

           A3: C = ( Cl ( Int B)) and

           A4: B in F;

          ( Int B) in ( Int F) by A4, Def1;

          hence X in ( Cl ( Int F)) by A3, PCOMPS_1:def 2;

        end;

        now

          assume

           A5: X in ( Cl ( Int F));

          then

          reconsider C = X as Subset of T;

          consider B be Subset of T such that

           A6: C = ( Cl B) and

           A7: B in ( Int F) by A5, PCOMPS_1:def 2;

          ex D be Subset of T st B = ( Int D) & D in F by A7, Def1;

          hence X in P by A6;

        end;

        hence thesis by A1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:32

    

     Th31: ( Int ( Cl F)) = { A where A be Subset of T : ex B be Subset of T st A = ( Int ( Cl B)) & B in F }

    proof

      set P = { A where A be Subset of T : ex B be Subset of T st A = ( Int ( Cl B)) & B in F };

      now

        let C be object;

        assume C in P;

        then ex A be Subset of T st C = A & ex B be Subset of T st A = ( Int ( Cl B)) & B in F;

        hence C in ( bool the carrier of T);

      end;

      then

      reconsider P as Subset-Family of T by TARSKI:def 3;

      reconsider P as Subset-Family of T;

      for X be object holds X in ( Int ( Cl F)) iff X in P

      proof

        let X be object;

         A1:

        now

          assume

           A2: X in P;

          then

          reconsider C = X as Subset of T;

          ex D be Subset of T st D = C & ex B be Subset of T st D = ( Int ( Cl B)) & B in F by A2;

          then

          consider B be Subset of T such that

           A3: C = ( Int ( Cl B)) and

           A4: B in F;

          ( Cl B) in ( Cl F) by A4, PCOMPS_1:def 2;

          hence X in ( Int ( Cl F)) by A3, Def1;

        end;

        now

          assume

           A5: X in ( Int ( Cl F));

          then

          reconsider C = X as Subset of T;

          consider B be Subset of T such that

           A6: C = ( Int B) and

           A7: B in ( Cl F) by A5, Def1;

          ex D be Subset of T st B = ( Cl D) & D in F by A7, PCOMPS_1:def 2;

          hence X in P by A6;

        end;

        hence thesis by A1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:33

    

     Th32: ( Cl ( Int ( Cl F))) = { A where A be Subset of T : ex B be Subset of T st A = ( Cl ( Int ( Cl B))) & B in F }

    proof

      set P = { A where A be Subset of T : ex B be Subset of T st A = ( Cl ( Int ( Cl B))) & B in F };

      now

        let C be object;

        assume C in P;

        then ex A be Subset of T st C = A & ex B be Subset of T st A = ( Cl ( Int ( Cl B))) & B in F;

        hence C in ( bool the carrier of T);

      end;

      then

      reconsider P as Subset-Family of T by TARSKI:def 3;

      reconsider P as Subset-Family of T;

      for X be object holds X in ( Cl ( Int ( Cl F))) iff X in P

      proof

        let X be object;

         A1:

        now

          assume

           A2: X in P;

          then

          reconsider C = X as Subset of T;

          ex D be Subset of T st D = C & ex B be Subset of T st D = ( Cl ( Int ( Cl B))) & B in F by A2;

          then

          consider B be Subset of T such that

           A3: C = ( Cl ( Int ( Cl B))) and

           A4: B in F;

          ( Cl B) in ( Cl F) by A4, PCOMPS_1:def 2;

          then ( Int ( Cl B)) in ( Int ( Cl F)) by Def1;

          hence X in ( Cl ( Int ( Cl F))) by A3, PCOMPS_1:def 2;

        end;

        now

          assume

           A5: X in ( Cl ( Int ( Cl F)));

          then

          reconsider C = X as Subset of T;

          consider B be Subset of T such that

           A6: C = ( Cl B) and

           A7: B in ( Int ( Cl F)) by A5, PCOMPS_1:def 2;

          consider D be Subset of T such that

           A8: B = ( Int D) and

           A9: D in ( Cl F) by A7, Def1;

          ex E be Subset of T st D = ( Cl E) & E in F by A9, PCOMPS_1:def 2;

          hence X in P by A6, A8;

        end;

        hence thesis by A1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:34

    

     Th33: ( Int ( Cl ( Int F))) = { A where A be Subset of T : ex B be Subset of T st A = ( Int ( Cl ( Int B))) & B in F }

    proof

      set P = { A where A be Subset of T : ex B be Subset of T st A = ( Int ( Cl ( Int B))) & B in F };

      now

        let C be object;

        assume C in P;

        then ex A be Subset of T st C = A & ex B be Subset of T st A = ( Int ( Cl ( Int B))) & B in F;

        hence C in ( bool the carrier of T);

      end;

      then

      reconsider P as Subset-Family of T by TARSKI:def 3;

      reconsider P as Subset-Family of T;

      for X be object holds X in ( Int ( Cl ( Int F))) iff X in P

      proof

        let X be object;

         A1:

        now

          assume

           A2: X in P;

          then

          reconsider C = X as Subset of T;

          ex D be Subset of T st D = C & ex B be Subset of T st D = ( Int ( Cl ( Int B))) & B in F by A2;

          then

          consider B be Subset of T such that

           A3: C = ( Int ( Cl ( Int B))) and

           A4: B in F;

          ( Int B) in ( Int F) by A4, Def1;

          then ( Cl ( Int B)) in ( Cl ( Int F)) by PCOMPS_1:def 2;

          hence X in ( Int ( Cl ( Int F))) by A3, Def1;

        end;

        now

          assume

           A5: X in ( Int ( Cl ( Int F)));

          then

          reconsider C = X as Subset of T;

          consider B be Subset of T such that

           A6: C = ( Int B) and

           A7: B in ( Cl ( Int F)) by A5, Def1;

          consider D be Subset of T such that

           A8: B = ( Cl D) and

           A9: D in ( Int F) by A7, PCOMPS_1:def 2;

          ex E be Subset of T st D = ( Int E) & E in F by A9, Def1;

          hence X in P by A6, A8;

        end;

        hence thesis by A1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:35

    ( Cl ( Int ( Cl ( Int F)))) = ( Cl ( Int F))

    proof

      set H = { A where A be Subset of T : ex B be Subset of T st A = ( Int ( Cl ( Int B))) & B in F };

      ( Int ( Cl ( Int F))) = H by Th33;

      then

      reconsider H as Subset-Family of T;

      

       A1: ( Cl ( Int ( Cl ( Int F)))) = ( Cl H) by Th33;

      

       A2: ( Cl ( Int F)) = { A where A be Subset of T : ex B be Subset of T st A = ( Cl ( Int B)) & B in F } by Th30;

      for X be object holds X in ( Cl ( Int ( Cl ( Int F)))) iff X in ( Cl ( Int F))

      proof

        let X be object;

         A3:

        now

          assume

           A4: X in ( Cl ( Int F));

          then

          reconsider C = X as Subset of T;

          ex D be Subset of T st D = C & ex B be Subset of T st D = ( Cl ( Int B)) & B in F by A2, A4;

          then

          consider B be Subset of T such that

           A5: C = ( Cl ( Int B)) and

           A6: B in F;

          ( Int B) in ( Int F) by A6, Def1;

          then ( Cl ( Int B)) in ( Cl ( Int F)) by PCOMPS_1:def 2;

          then

           A7: ( Int ( Cl ( Int B))) in ( Int ( Cl ( Int F))) by Def1;

          C = ( Cl ( Int ( Cl ( Int B)))) by A5, TOPS_1: 26;

          hence X in ( Cl ( Int ( Cl ( Int F)))) by A7, PCOMPS_1:def 2;

        end;

        now

          assume

           A8: X in ( Cl ( Int ( Cl ( Int F))));

          then

          reconsider C = X as Subset of T;

          consider B be Subset of T such that

           A9: C = ( Cl B) and

           A10: B in { A where A be Subset of T : ex B be Subset of T st A = ( Int ( Cl ( Int B))) & B in F } by A1, A8, PCOMPS_1:def 2;

          ex S be Subset of T st S = B & ex R be Subset of T st S = ( Int ( Cl ( Int R))) & R in F by A10;

          then

          consider D be Subset of T such that

           A11: B = ( Int ( Cl ( Int D))) and

           A12: D in F;

          

           A13: ( Int D) in ( Int F) by A12, Def1;

          C = ( Cl ( Int D)) by A9, A11, TOPS_1: 26;

          hence X in ( Cl ( Int F)) by A13, PCOMPS_1:def 2;

        end;

        hence thesis by A3;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:36

    ( Int ( Cl ( Int ( Cl F)))) = ( Int ( Cl F))

    proof

      set H = { A where A be Subset of T : ex B be Subset of T st A = ( Cl ( Int ( Cl B))) & B in F };

      ( Cl ( Int ( Cl F))) = H by Th32;

      then

      reconsider H as Subset-Family of T;

      

       A1: ( Int ( Cl ( Int ( Cl F)))) = ( Int H) by Th32;

      

       A2: ( Int ( Cl F)) = { A where A be Subset of T : ex B be Subset of T st A = ( Int ( Cl B)) & B in F } by Th31;

      for X be object holds X in ( Int ( Cl ( Int ( Cl F)))) iff X in ( Int ( Cl F))

      proof

        let X be object;

         A3:

        now

          assume

           A4: X in ( Int ( Cl F));

          then

          reconsider C = X as Subset of T;

          ex D be Subset of T st D = C & ex B be Subset of T st D = ( Int ( Cl B)) & B in F by A2, A4;

          then

          consider B be Subset of T such that

           A5: C = ( Int ( Cl B)) and

           A6: B in F;

          ( Cl B) in ( Cl F) by A6, PCOMPS_1:def 2;

          then ( Int ( Cl B)) in ( Int ( Cl F)) by Def1;

          then

           A7: ( Cl ( Int ( Cl B))) in ( Cl ( Int ( Cl F))) by PCOMPS_1:def 2;

          C = ( Int ( Cl ( Int ( Cl B)))) by A5, TDLAT_1: 5;

          hence X in ( Int ( Cl ( Int ( Cl F)))) by A7, Def1;

        end;

        now

          assume

           A8: X in ( Int ( Cl ( Int ( Cl F))));

          then

          reconsider C = X as Subset of T;

          consider B be Subset of T such that

           A9: C = ( Int B) and

           A10: B in { A where A be Subset of T : ex B be Subset of T st A = ( Cl ( Int ( Cl B))) & B in F } by A1, A8, Def1;

          ex S be Subset of T st S = B & ex R be Subset of T st S = ( Cl ( Int ( Cl R))) & R in F by A10;

          then

          consider D be Subset of T such that

           A11: B = ( Cl ( Int ( Cl D))) and

           A12: D in F;

          

           A13: ( Cl D) in ( Cl F) by A12, PCOMPS_1:def 2;

          C = ( Int ( Cl D)) by A9, A11, TDLAT_1: 5;

          hence X in ( Int ( Cl F)) by A13, Def1;

        end;

        hence thesis by A3;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TDLAT_2:37

    ( union ( Int ( Cl F))) c= ( union ( Cl ( Int ( Cl F))))

    proof

      now

        let x be object;

        assume x in ( union ( Int ( Cl F)));

        then

        consider A be set such that

         A1: x in A and

         A2: A in ( Int ( Cl F)) by TARSKI:def 4;

        reconsider A as Subset of T by A2;

        consider B be Subset of T such that

         A3: A = ( Int B) and

         A4: B in ( Cl F) by A2, Def1;

        consider D be Subset of T such that

         A5: B = ( Cl D) and

         A6: D in F by A4, PCOMPS_1:def 2;

        ex P be set st x in P & P in ( Cl ( Int ( Cl F)))

        proof

          take ( Cl ( Int ( Cl D)));

          ( Cl D) in ( Cl F) by A6, PCOMPS_1:def 2;

          then

           A7: ( Int ( Cl D)) in ( Int ( Cl F)) by Def1;

          A c= ( Cl ( Int ( Cl D))) by A3, A5, Th2;

          hence thesis by A1, A7, PCOMPS_1:def 2;

        end;

        hence x in ( union ( Cl ( Int ( Cl F)))) by TARSKI:def 4;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:38

    ( meet ( Int ( Cl F))) c= ( meet ( Cl ( Int ( Cl F))))

    proof

      now

        per cases ;

          suppose F = {} ;

          then ( Cl F) = {} by Th9;

          then ( Int ( Cl F)) = {} by Th18;

          hence thesis by Th9;

        end;

          suppose F <> {} ;

          then ( Cl F) <> {} by Th9;

          then ( Int ( Cl F)) <> {} by Th18;

          then

           A1: ( Cl ( Int ( Cl F))) <> {} by Th9;

          now

            let x be object;

            assume

             A2: x in ( meet ( Int ( Cl F)));

            for A be set st A in ( Cl ( Int ( Cl F))) holds x in A

            proof

              let A be set;

              assume

               A3: A in ( Cl ( Int ( Cl F)));

              then

              reconsider A as Subset of T;

              consider B be Subset of T such that

               A4: A = ( Cl B) and

               A5: B in ( Int ( Cl F)) by A3, PCOMPS_1:def 2;

              

               A6: B c= ( Cl B) by PRE_TOPC: 18;

              x in B by A2, A5, SETFAM_1:def 1;

              hence thesis by A4, A6;

            end;

            hence x in ( meet ( Cl ( Int ( Cl F)))) by A1, SETFAM_1:def 1;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:39

    ( union ( Cl ( Int F))) c= ( union ( Cl ( Int ( Cl F))))

    proof

      let x be object;

      assume x in ( union ( Cl ( Int F)));

      then

      consider A be set such that

       A1: x in A and

       A2: A in ( Cl ( Int F)) by TARSKI:def 4;

      reconsider A as Subset of T by A2;

      consider B be Subset of T such that

       A3: A = ( Cl B) and

       A4: B in ( Int F) by A2, PCOMPS_1:def 2;

      consider D be Subset of T such that

       A5: B = ( Int D) and

       A6: D in F by A4, Def1;

      ex P be set st x in P & P in ( Cl ( Int ( Cl F)))

      proof

        take ( Cl ( Int ( Cl D)));

        ( Cl D) in ( Cl F) by A6, PCOMPS_1:def 2;

        then

         A7: ( Int ( Cl D)) in ( Int ( Cl F)) by Def1;

        A c= ( Cl ( Int ( Cl D))) by A3, A5, Th2;

        hence thesis by A1, A7, PCOMPS_1:def 2;

      end;

      hence x in ( union ( Cl ( Int ( Cl F)))) by TARSKI:def 4;

    end;

    theorem :: TDLAT_2:40

    ( meet ( Cl ( Int F))) c= ( meet ( Cl ( Int ( Cl F))))

    proof

      now

        per cases ;

          suppose F = {} ;

          hence thesis by Th9;

        end;

          suppose F <> {} ;

          then ( Cl F) <> {} by Th9;

          then ( Int ( Cl F)) <> {} by Th18;

          then

           A1: ( Cl ( Int ( Cl F))) <> {} by Th9;

          now

            let x be object;

            assume

             A2: x in ( meet ( Cl ( Int F)));

            for A be set st A in ( Cl ( Int ( Cl F))) holds x in A

            proof

              let A be set;

              assume

               A3: A in ( Cl ( Int ( Cl F)));

              then

              reconsider A as Subset of T;

              consider B be Subset of T such that

               A4: A = ( Cl B) and

               A5: B in ( Int ( Cl F)) by A3, PCOMPS_1:def 2;

              consider D be Subset of T such that

               A6: B = ( Int D) and

               A7: D in ( Cl F) by A5, Def1;

              consider E be Subset of T such that

               A8: D = ( Cl E) and

               A9: E in F by A7, PCOMPS_1:def 2;

              ( Int E) in ( Int F) by A9, Def1;

              then ( Cl ( Int E)) in ( Cl ( Int F)) by PCOMPS_1:def 2;

              then

               A10: x in ( Cl ( Int E)) by A2, SETFAM_1:def 1;

              ( Cl ( Int E)) c= ( Cl ( Int ( Cl E))) by Th2;

              hence thesis by A4, A6, A8, A10;

            end;

            hence x in ( meet ( Cl ( Int ( Cl F)))) by A1, SETFAM_1:def 1;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:41

    ( union ( Int ( Cl ( Int F)))) c= ( union ( Int ( Cl F)))

    proof

      let x be object;

      assume x in ( union ( Int ( Cl ( Int F))));

      then

      consider A be set such that

       A1: x in A and

       A2: A in ( Int ( Cl ( Int F))) by TARSKI:def 4;

      reconsider A as Subset of T by A2;

      consider B be Subset of T such that

       A3: A = ( Int B) and

       A4: B in ( Cl ( Int F)) by A2, Def1;

      consider D be Subset of T such that

       A5: B = ( Cl D) and

       A6: D in ( Int F) by A4, PCOMPS_1:def 2;

      consider E be Subset of T such that

       A7: D = ( Int E) and

       A8: E in F by A6, Def1;

      ex P be set st x in P & P in ( Int ( Cl F))

      proof

        take ( Int ( Cl E));

        

         A9: ( Cl E) in ( Cl F) by A8, PCOMPS_1:def 2;

        A c= ( Int ( Cl E)) by A3, A5, A7, Th1;

        hence thesis by A1, A9, Def1;

      end;

      hence x in ( union ( Int ( Cl F))) by TARSKI:def 4;

    end;

    theorem :: TDLAT_2:42

    ( meet ( Int ( Cl ( Int F)))) c= ( meet ( Int ( Cl F)))

    proof

      now

        per cases ;

          suppose F = {} ;

          hence thesis by Th18;

        end;

          suppose F <> {} ;

          then ( Cl F) <> {} by Th9;

          then

           A1: ( Int ( Cl F)) <> {} by Th18;

          now

            let x be object;

            assume

             A2: x in ( meet ( Int ( Cl ( Int F))));

            for A be set st A in ( Int ( Cl F)) holds x in A

            proof

              let A be set;

              assume

               A3: A in ( Int ( Cl F));

              then

              reconsider A as Subset of T;

              consider E be Subset of T such that

               A4: A = ( Int E) and

               A5: E in ( Cl F) by A3, Def1;

              consider B be Subset of T such that

               A6: E = ( Cl B) and

               A7: B in F by A5, PCOMPS_1:def 2;

              ( Int B) in ( Int F) by A7, Def1;

              then ( Cl ( Int B)) in ( Cl ( Int F)) by PCOMPS_1:def 2;

              then ( Int ( Cl ( Int B))) in ( Int ( Cl ( Int F))) by Def1;

              then

               A8: x in ( Int ( Cl ( Int B))) by A2, SETFAM_1:def 1;

              ( Int ( Cl ( Int B))) c= ( Int ( Cl B)) by Th1;

              hence thesis by A4, A6, A8;

            end;

            hence x in ( meet ( Int ( Cl F))) by A1, SETFAM_1:def 1;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:43

    ( union ( Int ( Cl ( Int F)))) c= ( union ( Cl ( Int F)))

    proof

      let x be object;

      assume x in ( union ( Int ( Cl ( Int F))));

      then

      consider A be set such that

       A1: x in A and

       A2: A in ( Int ( Cl ( Int F))) by TARSKI:def 4;

      reconsider A as Subset of T by A2;

      consider B be Subset of T such that

       A3: A = ( Int B) and

       A4: B in ( Cl ( Int F)) by A2, Def1;

      consider D be Subset of T such that

       A5: B = ( Cl D) and

       A6: D in ( Int F) by A4, PCOMPS_1:def 2;

      consider E be Subset of T such that

       A7: D = ( Int E) and

       A8: E in F by A6, Def1;

      ex P be set st x in P & P in ( Cl ( Int F))

      proof

        take ( Cl ( Int E));

        

         A9: ( Int E) in ( Int F) by A8, Def1;

        A c= ( Cl ( Int E)) by A3, A5, A7, Th1;

        hence thesis by A1, A9, PCOMPS_1:def 2;

      end;

      hence x in ( union ( Cl ( Int F))) by TARSKI:def 4;

    end;

    theorem :: TDLAT_2:44

    ( meet ( Int ( Cl ( Int F)))) c= ( meet ( Cl ( Int F)))

    proof

      per cases ;

        suppose F = {} ;

        then ( Int F) = {} by Th18;

        then ( Cl ( Int F)) = {} by Th9;

        hence thesis by Th18;

      end;

        suppose F <> {} ;

        then ( Int F) <> {} by Th18;

        then

         A1: ( Cl ( Int F)) <> {} by Th9;

        now

          let x be object;

          assume

           A2: x in ( meet ( Int ( Cl ( Int F))));

          for A be set st A in ( Cl ( Int F)) holds x in A

          proof

            let A be set;

            assume

             A3: A in ( Cl ( Int F));

            then

            reconsider A as Subset of T;

            consider E be Subset of T such that

             A4: A = ( Cl E) and

             A5: E in ( Int F) by A3, PCOMPS_1:def 2;

            consider B be Subset of T such that

             A6: E = ( Int B) and

             A7: B in F by A5, Def1;

            ( Int B) in ( Int F) by A7, Def1;

            then ( Cl ( Int B)) in ( Cl ( Int F)) by PCOMPS_1:def 2;

            then ( Int ( Cl ( Int B))) in ( Int ( Cl ( Int F))) by Def1;

            then

             A8: x in ( Int ( Cl ( Int B))) by A2, SETFAM_1:def 1;

            ( Int ( Cl ( Int B))) c= ( Cl ( Int B)) by Th1;

            hence thesis by A4, A6, A8;

          end;

          hence x in ( meet ( Cl ( Int F))) by A1, SETFAM_1:def 1;

        end;

        hence thesis;

      end;

    end;

    theorem :: TDLAT_2:45

    ( union ( Cl ( Int ( Cl F)))) c= ( union ( Cl F))

    proof

      let x be object;

      assume x in ( union ( Cl ( Int ( Cl F))));

      then

      consider A be set such that

       A1: x in A and

       A2: A in ( Cl ( Int ( Cl F))) by TARSKI:def 4;

      reconsider A as Subset of T by A2;

      consider B be Subset of T such that

       A3: A = ( Cl B) and

       A4: B in ( Int ( Cl F)) by A2, PCOMPS_1:def 2;

      consider D be Subset of T such that

       A5: B = ( Int D) and

       A6: D in ( Cl F) by A4, Def1;

      consider E be Subset of T such that

       A7: D = ( Cl E) and

       A8: E in F by A6, PCOMPS_1:def 2;

      ex P be set st x in P & P in ( Cl F)

      proof

        take ( Cl E);

        A c= ( Cl E) by A3, A5, A7, TDLAT_1: 3;

        hence thesis by A1, A8, PCOMPS_1:def 2;

      end;

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

    end;

    theorem :: TDLAT_2:46

    ( meet ( Cl ( Int ( Cl F)))) c= ( meet ( Cl F))

    proof

      per cases ;

        suppose

         A1: F = {} ;

        then ( Cl F) = {} by Th9;

        hence thesis by A1, Th18;

      end;

        suppose F <> {} ;

        then

         A2: ( Cl F) <> {} by Th9;

        let x be object;

        assume

         A3: x in ( meet ( Cl ( Int ( Cl F))));

        for A be set st A in ( Cl F) holds x in A

        proof

          let A be set;

          assume

           A4: A in ( Cl F);

          then

          reconsider A as Subset of T;

          consider B be Subset of T such that

           A5: A = ( Cl B) and

           A6: B in F by A4, PCOMPS_1:def 2;

          ( Cl B) in ( Cl F) by A6, PCOMPS_1:def 2;

          then ( Int ( Cl B)) in ( Int ( Cl F)) by Def1;

          then ( Cl ( Int ( Cl B))) in ( Cl ( Int ( Cl F))) by PCOMPS_1:def 2;

          then

           A7: x in ( Cl ( Int ( Cl B))) by A3, SETFAM_1:def 1;

          ( Cl ( Int ( Cl B))) c= ( Cl B) by TDLAT_1: 3;

          hence thesis by A5, A7;

        end;

        hence x in ( meet ( Cl F)) by A2, SETFAM_1:def 1;

      end;

    end;

    theorem :: TDLAT_2:47

    ( union ( Int F)) c= ( union ( Int ( Cl ( Int F))))

    proof

      let x be object;

      assume x in ( union ( Int F));

      then

      consider A be set such that

       A1: x in A and

       A2: A in ( Int F) by TARSKI:def 4;

      reconsider A as Subset of T by A2;

      consider B be Subset of T such that

       A3: A = ( Int B) and

       A4: B in F by A2, Def1;

      ex P be set st x in P & P in ( Int ( Cl ( Int F)))

      proof

        take ( Int ( Cl ( Int B)));

        ( Int B) in ( Int F) by A4, Def1;

        then

         A5: ( Cl ( Int B)) in ( Cl ( Int F)) by PCOMPS_1:def 2;

        A c= ( Int ( Cl ( Int B))) by A3, TDLAT_1: 4;

        hence thesis by A1, A5, Def1;

      end;

      hence x in ( union ( Int ( Cl ( Int F)))) by TARSKI:def 4;

    end;

    theorem :: TDLAT_2:48

    ( meet ( Int F)) c= ( meet ( Int ( Cl ( Int F))))

    proof

      per cases ;

        suppose

         A1: F = {} ;

        then ( Int F) = {} by Th18;

        hence thesis by A1, Th9;

      end;

        suppose F <> {} ;

        then ( Int F) <> {} by Th18;

        then ( Cl ( Int F)) <> {} by Th9;

        then

         A2: ( Int ( Cl ( Int F))) <> {} by Th18;

        let x be object;

        assume

         A3: x in ( meet ( Int F));

        for A be set st A in ( Int ( Cl ( Int F))) holds x in A

        proof

          let A be set;

          assume

           A4: A in ( Int ( Cl ( Int F)));

          then

          reconsider A as Subset of T;

          consider E be Subset of T such that

           A5: A = ( Int E) and

           A6: E in ( Cl ( Int F)) by A4, Def1;

          consider B be Subset of T such that

           A7: E = ( Cl B) and

           A8: B in ( Int F) by A6, PCOMPS_1:def 2;

          consider D be Subset of T such that

           A9: B = ( Int D) and

           A10: D in F by A8, Def1;

          ( Int D) in ( Int F) by A10, Def1;

          then

           A11: x in ( Int D) by A3, SETFAM_1:def 1;

          ( Int D) c= ( Int ( Cl ( Int D))) by TDLAT_1: 4;

          hence thesis by A5, A7, A9, A11;

        end;

        hence x in ( meet ( Int ( Cl ( Int F)))) by A2, SETFAM_1:def 1;

      end;

    end;

    theorem :: TDLAT_2:49

    

     Th48: ( union ( Cl ( Int F))) c= ( Cl ( Int ( union F)))

    proof

      

       A1: ( Cl ( union ( Int F))) c= ( Cl ( Int ( union F))) by Th27, PRE_TOPC: 19;

      ( union ( Cl ( Int F))) c= ( Cl ( union ( Int F))) by Th15;

      hence thesis by A1;

    end;

    theorem :: TDLAT_2:50

    

     Th49: ( Cl ( Int ( meet F))) c= ( meet ( Cl ( Int F)))

    proof

      

       A1: ( Cl ( meet ( Int F))) c= ( meet ( Cl ( Int F))) by Th14;

      ( Cl ( Int ( meet F))) c= ( Cl ( meet ( Int F))) by Th28, PRE_TOPC: 19;

      hence thesis by A1;

    end;

    theorem :: TDLAT_2:51

    

     Th50: ( union ( Int ( Cl F))) c= ( Int ( Cl ( union F)))

    proof

      

       A1: ( Int ( union ( Cl F))) c= ( Int ( Cl ( union F))) by Th15, TOPS_1: 19;

      ( union ( Int ( Cl F))) c= ( Int ( union ( Cl F))) by Th27;

      hence thesis by A1;

    end;

    theorem :: TDLAT_2:52

    

     Th51: ( Int ( Cl ( meet F))) c= ( meet ( Int ( Cl F)))

    proof

      

       A1: ( Int ( meet ( Cl F))) c= ( meet ( Int ( Cl F))) by Th28;

      ( Int ( Cl ( meet F))) c= ( Int ( meet ( Cl F))) by Th14, TOPS_1: 19;

      hence thesis by A1;

    end;

    theorem :: TDLAT_2:53

    ( union ( Cl ( Int ( Cl F)))) c= ( Cl ( Int ( Cl ( union F))))

    proof

      

       A1: ( Cl ( union ( Int ( Cl F)))) c= ( Cl ( Int ( Cl ( union F)))) by Th50, PRE_TOPC: 19;

      ( union ( Cl ( Int ( Cl F)))) c= ( Cl ( union ( Int ( Cl F)))) by Th15;

      hence thesis by A1;

    end;

    theorem :: TDLAT_2:54

    ( Cl ( Int ( Cl ( meet F)))) c= ( meet ( Cl ( Int ( Cl F))))

    proof

      

       A1: ( Cl ( Int ( Cl ( meet F)))) c= ( Cl ( meet ( Int ( Cl F)))) by Th51, PRE_TOPC: 19;

      ( Cl ( meet ( Int ( Cl F)))) c= ( meet ( Cl ( Int ( Cl F)))) by Th14;

      hence thesis by A1;

    end;

    theorem :: TDLAT_2:55

    ( union ( Int ( Cl ( Int F)))) c= ( Int ( Cl ( Int ( union F))))

    proof

      

       A1: ( Int ( union ( Cl ( Int F)))) c= ( Int ( Cl ( Int ( union F)))) by Th48, TOPS_1: 19;

      ( union ( Int ( Cl ( Int F)))) c= ( Int ( union ( Cl ( Int F)))) by Th27;

      hence thesis by A1;

    end;

    theorem :: TDLAT_2:56

    ( Int ( Cl ( Int ( meet F)))) c= ( meet ( Int ( Cl ( Int F))))

    proof

      

       A1: ( Int ( Cl ( Int ( meet F)))) c= ( Int ( meet ( Cl ( Int F)))) by Th49, TOPS_1: 19;

      ( Int ( meet ( Cl ( Int F)))) c= ( meet ( Int ( Cl ( Int F)))) by Th28;

      hence thesis by A1;

    end;

    theorem :: TDLAT_2:57

    

     Th56: for F be Subset-Family of T holds (for A be Subset of T st A in F holds A c= ( Cl ( Int A))) implies ( union F) c= ( Cl ( Int ( union F))) & ( Cl ( union F)) = ( Cl ( Int ( Cl ( union F))))

    proof

      let F be Subset-Family of T;

      

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

      assume

       A2: for A be Subset of T st A in F holds A c= ( Cl ( Int A));

       A3:

      now

        let A0 be set;

        assume

         A4: A0 in F;

        then

        reconsider A = A0 as Subset of T;

        ( Int A) c= ( Int ( union F)) by A4, TOPS_1: 19, ZFMISC_1: 74;

        then

         A5: ( Cl ( Int A)) c= ( Cl ( Int ( union F))) by PRE_TOPC: 19;

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

        hence A0 c= ( Cl ( Int ( union F))) by A5;

      end;

      hence ( union F) c= ( Cl ( Int ( union F))) by ZFMISC_1: 76;

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

      then

       A6: ( Cl ( Int ( union F))) c= ( Cl ( Int ( Cl ( union F)))) by PRE_TOPC: 19;

      ( union F) c= ( Cl ( Int ( union F))) by A3, ZFMISC_1: 76;

      then ( Cl ( union F)) c= ( Cl ( Cl ( Int ( union F)))) by PRE_TOPC: 19;

      then ( Cl ( union F)) c= ( Cl ( Int ( Cl ( union F)))) by A6;

      hence ( Cl ( union F)) = ( Cl ( Int ( Cl ( union F)))) by A1, XBOOLE_0:def 10;

    end;

    theorem :: TDLAT_2:58

    

     Th57: for F be Subset-Family of T holds (for A be Subset of T st A in F holds ( Int ( Cl A)) c= A) implies ( Int ( Cl ( meet F))) c= ( meet F) & ( Int ( Cl ( Int ( meet F)))) = ( Int ( meet F))

    proof

      let F be Subset-Family of T;

      

       A1: ( Int ( Int ( meet F))) c= ( Int ( Cl ( Int ( meet F)))) by PRE_TOPC: 18, TOPS_1: 19;

      assume

       A2: for A be Subset of T st A in F holds ( Int ( Cl A)) c= A;

      thus ( Int ( Cl ( meet F))) c= ( meet F)

      proof

        now

          per cases ;

            suppose

             A3: F = {} ;

            ( Cl ( {} T)) = ( {} T) by PRE_TOPC: 22;

            hence thesis by A3, SETFAM_1: 1;

          end;

            suppose

             A4: F <> {} ;

            now

              let A0 be set;

              assume

               A5: A0 in F;

              then

              reconsider A = A0 as Subset of T;

              ( Cl ( meet F)) c= ( Cl A) by A5, PRE_TOPC: 19, SETFAM_1: 3;

              then

               A6: ( Int ( Cl ( meet F))) c= ( Int ( Cl A)) by TOPS_1: 19;

              ( Int ( Cl A)) c= A by A2, A5;

              hence ( Int ( Cl ( meet F))) c= A0 by A6;

            end;

            hence thesis by A4, SETFAM_1: 5;

          end;

        end;

        hence thesis;

      end;

      then

       A7: ( Int ( Int ( Cl ( meet F)))) c= ( Int ( meet F)) by TOPS_1: 19;

      ( Cl ( Int ( meet F))) c= ( Cl ( meet F)) by PRE_TOPC: 19, TOPS_1: 16;

      then ( Int ( Cl ( Int ( meet F)))) c= ( Int ( Cl ( meet F))) by TOPS_1: 19;

      then ( Int ( Cl ( Int ( meet F)))) c= ( Int ( meet F)) by A7;

      hence ( Int ( Cl ( Int ( meet F)))) = ( Int ( meet F)) by A1, XBOOLE_0:def 10;

    end;

    begin

    reserve T for non empty TopSpace;

    theorem :: TDLAT_2:59

    

     Th58: for A,B be Subset of T st B is condensed holds (( Int ( Cl (A \/ B))) \/ (A \/ B)) = B iff A c= B

    proof

      let A,B be Subset of T;

      assume

       A1: B is condensed;

      thus (( Int ( Cl (A \/ B))) \/ (A \/ B)) = B implies A c= B

      proof

        assume (( Int ( Cl (A \/ B))) \/ (A \/ B)) = B;

        then

         A2: (A \/ B) c= B by XBOOLE_1: 7;

        A c= (A \/ B) by XBOOLE_1: 7;

        hence thesis by A2;

      end;

      thus A c= B implies (( Int ( Cl (A \/ B))) \/ (A \/ B)) = B

      proof

        assume A c= B;

        then

         A3: (A \/ B) = B by XBOOLE_1: 12;

        then ( Int ( Cl (A \/ B))) c= B by A1, TOPS_1:def 6;

        hence thesis by A3, XBOOLE_1: 12;

      end;

    end;

    theorem :: TDLAT_2:60

    for A,B be Subset of T st A is condensed holds (( Cl ( Int (A /\ B))) /\ (A /\ B)) = A iff A c= B

    proof

      let A,B be Subset of T;

      assume

       A1: A is condensed;

      thus (( Cl ( Int (A /\ B))) /\ (A /\ B)) = A implies A c= B

      proof

        assume (( Cl ( Int (A /\ B))) /\ (A /\ B)) = A;

        then

         A2: A c= (A /\ B) by XBOOLE_1: 17;

        (A /\ B) c= B by XBOOLE_1: 17;

        hence thesis by A2;

      end;

      thus A c= B implies (( Cl ( Int (A /\ B))) /\ (A /\ B)) = A

      proof

        assume A c= B;

        then

         A3: (A /\ B) = A by XBOOLE_1: 28;

        then A c= ( Cl ( Int (A /\ B))) by A1, TOPS_1:def 6;

        hence thesis by A3, XBOOLE_1: 28;

      end;

    end;

    theorem :: TDLAT_2:61

    for A,B be Subset of T st A is closed_condensed & B is closed_condensed holds ( Int A) c= ( Int B) iff A c= B

    proof

      let A,B be Subset of T;

      assume that

       A1: A is closed_condensed and

       A2: B is closed_condensed;

      thus ( Int A) c= ( Int B) implies A c= B

      proof

        assume ( Int A) c= ( Int B);

        then

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

        ( Cl ( Int A)) = A by A1, TOPS_1:def 7;

        hence thesis by A2, A3, TOPS_1:def 7;

      end;

      thus thesis by TOPS_1: 19;

    end;

    theorem :: TDLAT_2:62

    for A,B be Subset of T st A is open_condensed & B is open_condensed holds ( Cl A) c= ( Cl B) iff A c= B

    proof

      let A,B be Subset of T;

      assume that

       A1: A is open_condensed and

       A2: B is open_condensed;

      thus ( Cl A) c= ( Cl B) implies A c= B

      proof

        assume ( Cl A) c= ( Cl B);

        then

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

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

        hence thesis by A2, A3, TOPS_1:def 8;

      end;

      thus thesis by PRE_TOPC: 19;

    end;

    theorem :: TDLAT_2:63

    for A,B be Subset of T st A is closed_condensed holds A c= B implies ( Cl ( Int (A /\ B))) = A

    proof

      let A,B be Subset of T;

      assume

       A1: A is closed_condensed;

      assume A c= B;

      then (A /\ B) = A by XBOOLE_1: 28;

      hence thesis by A1, TOPS_1:def 7;

    end;

    theorem :: TDLAT_2:64

    

     Th63: for A,B be Subset of T st B is open_condensed holds A c= B implies ( Int ( Cl (A \/ B))) = B

    proof

      let A,B be Subset of T;

      assume

       A1: B is open_condensed;

      assume A c= B;

      then (A \/ B) = B by XBOOLE_1: 12;

      hence thesis by A1, TOPS_1:def 8;

    end;

    definition

      let T;

      let IT be Subset-Family of T;

      :: TDLAT_2:def2

      attr IT is domains-family means for A be Subset of T holds A in IT implies A is condensed;

    end

    theorem :: TDLAT_2:65

    

     Th64: for F be Subset-Family of T holds F c= ( Domains_of T) iff F is domains-family

    proof

      let F be Subset-Family of T;

      thus F c= ( Domains_of T) implies F is domains-family

      proof

        assume

         A1: F c= ( Domains_of T);

        now

          let A be Subset of T;

          assume A in F;

          then A in ( Domains_of T) by A1;

          then A in { P where P be Subset of T : P is condensed } by TDLAT_1:def 1;

          then ex Q be Subset of T st Q = A & Q is condensed;

          hence A is condensed;

        end;

        hence thesis;

      end;

      thus F is domains-family implies F c= ( Domains_of T)

      proof

        assume

         A2: F is domains-family;

        for X be object holds X in F implies X in ( Domains_of T)

        proof

          let X be object;

          assume

           A3: X in F;

          then

          reconsider X0 = X as Subset of T;

          X0 is condensed by A2, A3;

          then X0 in { P where P be Subset of T : P is condensed };

          hence thesis by TDLAT_1:def 1;

        end;

        hence thesis;

      end;

    end;

    theorem :: TDLAT_2:66

    

     Th65: for F be Subset-Family of T holds F is domains-family implies ( union F) c= ( Cl ( Int ( union F))) & ( Cl ( union F)) = ( Cl ( Int ( Cl ( union F))))

    proof

      let F be Subset-Family of T;

      assume

       A1: F is domains-family;

      now

        let A be Subset of T;

        reconsider B = A as Subset of T;

        assume A in F;

        then B is condensed by A1;

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

      end;

      hence thesis by Th56;

    end;

    theorem :: TDLAT_2:67

    

     Th66: for F be Subset-Family of T holds F is domains-family implies ( Int ( Cl ( meet F))) c= ( meet F) & ( Int ( Cl ( Int ( meet F)))) = ( Int ( meet F))

    proof

      let F be Subset-Family of T;

      assume

       A1: F is domains-family;

      now

        let A be Subset of T;

        reconsider B = A as Subset of T;

        assume A in F;

        then B is condensed by A1;

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

      end;

      hence thesis by Th57;

    end;

    theorem :: TDLAT_2:68

    

     Th67: for F be Subset-Family of T holds F is domains-family implies (( union F) \/ ( Int ( Cl ( union F)))) is condensed

    proof

      let F be Subset-Family of T;

      

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

      assume F is domains-family;

      then ( union F) c= ( Cl ( Int ( union F))) by Th65;

      then

       A2: (( union F) \/ ( Int ( Cl ( union F)))) c= ( Cl ( Int (( union F) \/ ( Int ( Cl ( union F)))))) by Th5;

      ( Int ( Cl (( union F) \/ ( Int ( Cl ( union F)))))) = ( Int (( Cl ( union F)) \/ ( Cl ( Int ( Cl ( union F)))))) by PRE_TOPC: 20

      .= ( Int ( Cl ( union F))) by A1, XBOOLE_1: 12;

      then ( Int ( Cl (( union F) \/ ( Int ( Cl ( union F)))))) c= (( union F) \/ ( Int ( Cl ( union F)))) by XBOOLE_1: 7;

      hence thesis by A2, TOPS_1:def 6;

    end;

    theorem :: TDLAT_2:69

    

     Th68: for F be Subset-Family of T holds (for B be Subset of T st B in F holds B c= (( union F) \/ ( Int ( Cl ( union F))))) & for A be Subset of T st A is condensed holds (for B be Subset of T st B in F holds B c= A) implies (( union F) \/ ( Int ( Cl ( union F)))) c= A

    proof

      let F be Subset-Family of T;

      thus for B be Subset of T st B in F holds B c= (( union F) \/ ( Int ( Cl ( union F))))

      proof

        let B be Subset of T;

        assume B in F;

        then

         A1: B c= ( union F) by ZFMISC_1: 74;

        ( union F) c= (( union F) \/ ( Int ( Cl ( union F)))) by XBOOLE_1: 7;

        hence thesis by A1;

      end;

      thus for A be Subset of T st A is condensed holds (for B be Subset of T st B in F holds B c= A) implies (( union F) \/ ( Int ( Cl ( union F)))) c= A

      proof

        let A be Subset of T;

        assume A is condensed;

        then

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

        assume for B be Subset of T st B in F holds B c= A;

        then for P be set st P in F holds P c= A;

        then

         A3: ( union F) c= A by ZFMISC_1: 76;

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

        then ( Int ( Cl ( union F))) c= ( Int ( Cl A)) by TOPS_1: 19;

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

        hence thesis by A3, XBOOLE_1: 8;

      end;

    end;

    theorem :: TDLAT_2:70

    

     Th69: for F be Subset-Family of T holds F is domains-family implies (( meet F) /\ ( Cl ( Int ( meet F)))) is condensed

    proof

      let F be Subset-Family of T;

      

       A1: ( Int ( Int ( meet F))) c= ( Int ( Cl ( Int ( meet F)))) by PRE_TOPC: 18, TOPS_1: 19;

      assume F is domains-family;

      then ( Int ( Cl ( meet F))) c= ( meet F) by Th66;

      then

       A2: ( Int ( Cl (( meet F) /\ ( Cl ( Int ( meet F)))))) c= (( meet F) /\ ( Cl ( Int ( meet F)))) by Th6;

      ( Cl ( Int (( meet F) /\ ( Cl ( Int ( meet F)))))) = ( Cl (( Int ( meet F)) /\ ( Int ( Cl ( Int ( meet F)))))) by TOPS_1: 17

      .= ( Cl ( Int ( meet F))) by A1, XBOOLE_1: 28;

      then (( meet F) /\ ( Cl ( Int ( meet F)))) c= ( Cl ( Int (( meet F) /\ ( Cl ( Int ( meet F)))))) by XBOOLE_1: 17;

      hence thesis by A2, TOPS_1:def 6;

    end;

    theorem :: TDLAT_2:71

    

     Th70: for F be Subset-Family of T holds (for B be Subset of T st B in F holds (( meet F) /\ ( Cl ( Int ( meet F)))) c= B) & (F = {} or for A be Subset of T st A is condensed holds (for B be Subset of T st B in F holds A c= B) implies A c= (( meet F) /\ ( Cl ( Int ( meet F)))))

    proof

      let F be Subset-Family of T;

      thus for B be Subset of T st B in F holds (( meet F) /\ ( Cl ( Int ( meet F)))) c= B

      proof

        let B be Subset of T;

        assume B in F;

        then

         A1: ( meet F) c= B by SETFAM_1: 3;

        (( meet F) /\ ( Cl ( Int ( meet F)))) c= ( meet F) by XBOOLE_1: 17;

        hence thesis by A1;

      end;

      thus F = {} or for A be Subset of T st A is condensed holds (for B be Subset of T st B in F holds A c= B) implies A c= (( meet F) /\ ( Cl ( Int ( meet F))))

      proof

        assume

         A2: F <> {} ;

        let A be Subset of T;

        assume A is condensed;

        then

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

        assume for B be Subset of T st B in F holds A c= B;

        then for P be set st P in F holds A c= P;

        then

         A4: A c= ( meet F) by A2, SETFAM_1: 5;

        then ( Int A) c= ( Int ( meet F)) by TOPS_1: 19;

        then ( Cl ( Int A)) c= ( Cl ( Int ( meet F))) by PRE_TOPC: 19;

        then A c= ( Cl ( Int ( meet F))) by A3;

        hence thesis by A4, XBOOLE_1: 19;

      end;

    end;

    definition

      let T;

      let IT be Subset-Family of T;

      :: TDLAT_2:def3

      attr IT is closed-domains-family means for A be Subset of T holds A in IT implies A is closed_condensed;

    end

    theorem :: TDLAT_2:72

    

     Th71: for F be Subset-Family of T holds F c= ( Closed_Domains_of T) iff F is closed-domains-family

    proof

      let F be Subset-Family of T;

      thus F c= ( Closed_Domains_of T) implies F is closed-domains-family

      proof

        assume

         A1: F c= ( Closed_Domains_of T);

        now

          let A be Subset of T;

          assume A in F;

          then A in ( Closed_Domains_of T) by A1;

          then A in { P where P be Subset of T : P is closed_condensed } by TDLAT_1:def 5;

          then ex Q be Subset of T st Q = A & Q is closed_condensed;

          hence A is closed_condensed;

        end;

        hence thesis;

      end;

      thus F is closed-domains-family implies F c= ( Closed_Domains_of T)

      proof

        assume

         A2: F is closed-domains-family;

        for X be object holds X in F implies X in ( Closed_Domains_of T)

        proof

          let X be object;

          assume

           A3: X in F;

          then

          reconsider X0 = X as Subset of T;

          X0 is closed_condensed by A2, A3;

          then X0 in { P where P be Subset of T : P is closed_condensed };

          hence thesis by TDLAT_1:def 5;

        end;

        hence thesis;

      end;

    end;

    theorem :: TDLAT_2:73

    

     Th72: for F be Subset-Family of T holds F is closed-domains-family implies F is domains-family

    proof

      let F be Subset-Family of T;

      thus F is closed-domains-family implies F is domains-family

      proof

        assume F is closed-domains-family;

        then

         A1: F c= ( Closed_Domains_of T) by Th71;

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

        then F c= ( Domains_of T) by A1;

        hence thesis by Th64;

      end;

    end;

    theorem :: TDLAT_2:74

    

     Th73: for F be Subset-Family of T holds F is closed-domains-family implies F is closed

    proof

      let F be Subset-Family of T;

      assume

       A1: F is closed-domains-family;

      for A be Subset of T holds A in F implies A is closed

      proof

        let A be Subset of T;

        assume A in F;

        then A is closed_condensed by A1;

        hence thesis by TOPS_1: 66;

      end;

      hence thesis by TOPS_2:def 2;

    end;

    theorem :: TDLAT_2:75

    for F be Subset-Family of T holds F is domains-family implies ( Cl F) is closed-domains-family

    proof

      let F be Subset-Family of T;

      assume

       A1: F is domains-family;

      for A be Subset of T holds A in ( Cl F) implies A is closed_condensed

      proof

        let A be Subset of T;

        assume A in ( Cl F);

        then

        consider P be Subset of T such that

         A2: A = ( Cl P) and

         A3: P in F by PCOMPS_1:def 2;

        reconsider P as Subset of T;

        P is condensed by A1, A3;

        hence thesis by A2, TDLAT_1: 24;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:76

    

     Th75: for F be Subset-Family of T holds F is closed-domains-family implies ( Cl ( union F)) is closed_condensed & ( Cl ( Int ( meet F))) is closed_condensed

    proof

      let F be Subset-Family of T;

      assume F is closed-domains-family;

      then F is domains-family by Th72;

      then ( Cl ( union F)) = ( Cl ( Int ( Cl ( union F)))) by Th65;

      hence ( Cl ( union F)) is closed_condensed by TOPS_1:def 7;

      thus thesis by TDLAT_1: 22;

    end;

    theorem :: TDLAT_2:77

    

     Th76: for F be Subset-Family of T holds (for B be Subset of T st B in F holds B c= ( Cl ( union F))) & for A be Subset of T st A is closed_condensed holds (for B be Subset of T st B in F holds B c= A) implies ( Cl ( union F)) c= A

    proof

      let F be Subset-Family of T;

      thus for B be Subset of T st B in F holds B c= ( Cl ( union F))

      proof

        let B be Subset of T;

        assume B in F;

        then

         A1: B c= ( union F) by ZFMISC_1: 74;

        ( union F) c= ( Cl ( union F)) by PRE_TOPC: 18;

        hence thesis by A1;

      end;

      thus for A be Subset of T st A is closed_condensed holds (for B be Subset of T st B in F holds B c= A) implies ( Cl ( union F)) c= A

      proof

        let A be Subset of T;

        reconsider A1 = A as Subset of T;

        assume A is closed_condensed;

        then

         A2: A1 is closed by TOPS_1: 66;

        assume for B be Subset of T st B in F holds B c= A;

        then for P be set st P in F holds P c= A;

        then ( union F) c= A by ZFMISC_1: 76;

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

        hence thesis by A2, PRE_TOPC: 22;

      end;

    end;

    theorem :: TDLAT_2:78

    

     Th77: for F be Subset-Family of T holds (F is closed implies for B be Subset of T st B in F holds ( Cl ( Int ( meet F))) c= B) & (F = {} or for A be Subset of T st A is closed_condensed holds (for B be Subset of T st B in F holds A c= B) implies A c= ( Cl ( Int ( meet F))))

    proof

      let F be Subset-Family of T;

      thus F is closed implies for B be Subset of T st B in F holds ( Cl ( Int ( meet F))) c= B

      proof

        assume F is closed;

        then ( meet F) is closed by TOPS_2: 22;

        then

         A1: ( Cl ( meet F)) = ( meet F) by PRE_TOPC: 22;

        let B be Subset of T;

        

         A2: ( Cl ( Int ( meet F))) c= ( Cl ( meet F)) by PRE_TOPC: 19, TOPS_1: 16;

        assume B in F;

        then ( meet F) c= B by SETFAM_1: 3;

        hence thesis by A2, A1;

      end;

      thus F = {} or for A be Subset of T st A is closed_condensed holds (for B be Subset of T st B in F holds A c= B) implies A c= ( Cl ( Int ( meet F)))

      proof

        assume

         A3: F <> {} ;

        let A be Subset of T;

        assume

         A4: A is closed_condensed;

        assume for B be Subset of T st B in F holds A c= B;

        then for P be set st P in F holds A c= P;

        then A c= ( meet F) by A3, SETFAM_1: 5;

        then

         A5: ( Int A) c= ( Int ( meet F)) by TOPS_1: 19;

        A = ( Cl ( Int A)) by A4, TOPS_1:def 7;

        hence thesis by A5, PRE_TOPC: 19;

      end;

    end;

    definition

      let T;

      let IT be Subset-Family of T;

      :: TDLAT_2:def4

      attr IT is open-domains-family means for A be Subset of T holds A in IT implies A is open_condensed;

    end

    theorem :: TDLAT_2:79

    

     Th78: for F be Subset-Family of T holds F c= ( Open_Domains_of T) iff F is open-domains-family

    proof

      let F be Subset-Family of T;

      thus F c= ( Open_Domains_of T) implies F is open-domains-family

      proof

        assume

         A1: F c= ( Open_Domains_of T);

        now

          let A be Subset of T;

          assume A in F;

          then A in ( Open_Domains_of T) by A1;

          then A in { P where P be Subset of T : P is open_condensed } by TDLAT_1:def 9;

          then ex Q be Subset of T st Q = A & Q is open_condensed;

          hence A is open_condensed;

        end;

        hence thesis;

      end;

      thus F is open-domains-family implies F c= ( Open_Domains_of T)

      proof

        assume

         A2: F is open-domains-family;

        for X be object holds X in F implies X in ( Open_Domains_of T)

        proof

          let X be object;

          assume

           A3: X in F;

          then

          reconsider X0 = X as Subset of T;

          X0 is open_condensed by A2, A3;

          then X0 in { P where P be Subset of T : P is open_condensed };

          hence thesis by TDLAT_1:def 9;

        end;

        hence thesis;

      end;

    end;

    theorem :: TDLAT_2:80

    

     Th79: for F be Subset-Family of T holds F is open-domains-family implies F is domains-family

    proof

      let F be Subset-Family of T;

      thus F is open-domains-family implies F is domains-family

      proof

        assume F is open-domains-family;

        then

         A1: F c= ( Open_Domains_of T) by Th78;

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

        then F c= ( Domains_of T) by A1;

        hence thesis by Th64;

      end;

    end;

    theorem :: TDLAT_2:81

    

     Th80: for F be Subset-Family of T holds F is open-domains-family implies F is open

    proof

      let F be Subset-Family of T;

      assume

       A1: F is open-domains-family;

      for A be Subset of T holds A in F implies A is open

      proof

        let A be Subset of T;

        assume A in F;

        then A is open_condensed by A1;

        hence thesis by TOPS_1: 67;

      end;

      hence thesis by TOPS_2:def 1;

    end;

    theorem :: TDLAT_2:82

    for F be Subset-Family of T holds F is domains-family implies ( Int F) is open-domains-family

    proof

      let F be Subset-Family of T;

      assume

       A1: F is domains-family;

      for A be Subset of T holds A in ( Int F) implies A is open_condensed

      proof

        let A be Subset of T;

        assume A in ( Int F);

        then

        consider P be Subset of T such that

         A2: A = ( Int P) and

         A3: P in F by Def1;

        reconsider P as Subset of T;

        P is condensed by A1, A3;

        hence thesis by A2, TDLAT_1: 25;

      end;

      hence thesis;

    end;

    theorem :: TDLAT_2:83

    

     Th82: for F be Subset-Family of T holds F is open-domains-family implies ( Int ( meet F)) is open_condensed & ( Int ( Cl ( union F))) is open_condensed

    proof

      let F be Subset-Family of T;

      assume F is open-domains-family;

      then F is domains-family by Th79;

      then ( Int ( Cl ( Int ( meet F)))) = ( Int ( meet F)) by Th66;

      hence ( Int ( meet F)) is open_condensed by TOPS_1:def 8;

      thus thesis by TDLAT_1: 23;

    end;

    theorem :: TDLAT_2:84

    

     Th83: for F be Subset-Family of T holds (F is open implies for B be Subset of T st B in F holds B c= ( Int ( Cl ( union F)))) & for A be Subset of T st A is open_condensed holds (for B be Subset of T st B in F holds B c= A) implies ( Int ( Cl ( union F))) c= A

    proof

      let F be Subset-Family of T;

      thus F is open implies for B be Subset of T st B in F holds B c= ( Int ( Cl ( union F)))

      proof

        assume F is open;

        then ( union F) is open by TOPS_2: 19;

        then

         A1: ( Int ( union F)) = ( union F) by TOPS_1: 23;

        let B be Subset of T;

        

         A2: ( Int ( union F)) c= ( Int ( Cl ( union F))) by PRE_TOPC: 18, TOPS_1: 19;

        assume B in F;

        then B c= ( union F) by ZFMISC_1: 74;

        hence thesis by A2, A1;

      end;

      thus for A be Subset of T st A is open_condensed holds (for B be Subset of T st B in F holds B c= A) implies ( Int ( Cl ( union F))) c= A

      proof

        let A be Subset of T;

        assume A is open_condensed;

        then

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

        assume for B be Subset of T st B in F holds B c= A;

        then for P be set st P in F holds P c= A;

        then ( union F) c= A by ZFMISC_1: 76;

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

        hence thesis by A3, TOPS_1: 19;

      end;

    end;

    theorem :: TDLAT_2:85

    

     Th84: for F be Subset-Family of T holds (for B be Subset of T st B in F holds ( Int ( meet F)) c= B) & (F = {} or for A be Subset of T st A is open_condensed holds (for B be Subset of T st B in F holds A c= B) implies A c= ( Int ( meet F)))

    proof

      let F be Subset-Family of T;

      thus for B be Subset of T st B in F holds ( Int ( meet F)) c= B

      proof

        let B be Subset of T;

        assume B in F;

        then

         A1: ( meet F) c= B by SETFAM_1: 3;

        ( Int ( meet F)) c= ( meet F) by TOPS_1: 16;

        hence thesis by A1;

      end;

      thus F = {} or for A be Subset of T st A is open_condensed holds (for B be Subset of T st B in F holds A c= B) implies A c= ( Int ( meet F))

      proof

        assume

         A2: F <> {} ;

        let A be Subset of T;

        assume

         A3: A is open_condensed;

        assume for B be Subset of T st B in F holds A c= B;

        then for P be set st P in F holds A c= P;

        then

         A4: A c= ( meet F) by A2, SETFAM_1: 5;

        A is open by A3, TOPS_1: 67;

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

        hence thesis by A4, TOPS_1: 19;

      end;

    end;

    begin

    reserve T for non empty TopSpace;

    theorem :: TDLAT_2:86

    

     Th85: the carrier of ( Domains_Lattice T) = ( Domains_of T)

    proof

      ( Domains_Lattice T) = LattStr (# ( Domains_of T), ( D-Union T), ( D-Meet T) #) by TDLAT_1:def 4;

      hence thesis;

    end;

    theorem :: TDLAT_2:87

    

     Th86: for a,b be Element of ( Domains_Lattice T) holds for A,B be Element of ( Domains_of T) st a = A & b = B holds (a "\/" b) = (( Int ( Cl (A \/ B))) \/ (A \/ B)) & (a "/\" b) = (( Cl ( Int (A /\ B))) /\ (A /\ B))

    proof

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

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

      assume that

       A1: a = A and

       A2: b = B;

      

       A3: ( Domains_Lattice T) = LattStr (# ( Domains_of T), ( D-Union T), ( D-Meet T) #) by TDLAT_1:def 4;

      

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

      .= (( Int ( Cl (A \/ B))) \/ (A \/ B)) by TDLAT_1:def 2;

      

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

      .= (( Cl ( Int (A /\ B))) /\ (A /\ B)) by TDLAT_1:def 3;

    end;

    theorem :: TDLAT_2:88

    ( Bottom ( Domains_Lattice T)) = ( {} T) & ( Top ( Domains_Lattice T)) = ( [#] T)

    proof

      thus ( Bottom ( Domains_Lattice T)) = ( {} T)

      proof

        ( {} T) is condensed by TDLAT_1: 14;

        then

         A1: ( {} T) in { A where A be Subset of T : A is condensed };

        then

        reconsider E = ( {} T) as Element of ( Domains_of T) by TDLAT_1:def 1;

        ( {} T) in ( Domains_of T) by A1, TDLAT_1:def 1;

        then

        reconsider e = ( {} T) as Element of ( Domains_Lattice T) by Th85;

        for a be Element of ( Domains_Lattice T) holds (e "\/" a) = a

        proof

          let a be Element of ( Domains_Lattice T);

          reconsider A = a as Element of ( Domains_of T) by Th85;

          A in ( Domains_of T);

          then A in { C where C be Subset of T : C is condensed } by TDLAT_1:def 1;

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

          then

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

          

          thus (e "\/" a) = (( Int ( Cl (E \/ A))) \/ (E \/ A)) by Th86

          .= a by A2, XBOOLE_1: 12;

        end;

        hence thesis by LATTICE2: 14;

      end;

      thus ( Top ( Domains_Lattice T)) = ( [#] T)

      proof

        ( [#] T) is condensed by TDLAT_1: 15;

        then

         A3: ( [#] T) in { A where A be Subset of T : A is condensed };

        then

        reconsider E = ( [#] T) as Element of ( Domains_of T) by TDLAT_1:def 1;

        ( [#] T) in ( Domains_of T) by A3, TDLAT_1:def 1;

        then

        reconsider e = ( [#] T) as Element of ( Domains_Lattice T) by Th85;

        for a be Element of ( Domains_Lattice T) holds (e "/\" a) = a

        proof

          let a be Element of ( Domains_Lattice T);

          reconsider A = a as Element of ( Domains_of T) by Th85;

          A in ( Domains_of T);

          then A in { C where C be Subset of T : C is condensed } by TDLAT_1:def 1;

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

          then

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

          

          thus (e "/\" a) = (( Cl ( Int (E /\ A))) /\ (E /\ A)) by Th86

          .= (( Cl ( Int A)) /\ (( [#] T) /\ A)) by XBOOLE_1: 28

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

          .= a by A4, XBOOLE_1: 28;

        end;

        hence thesis by LATTICE2: 16;

      end;

    end;

    theorem :: TDLAT_2:89

    

     Th88: for a,b be Element of ( Domains_Lattice T) holds for A,B be Element of ( Domains_of T) st a = A & b = B holds a [= b iff A c= B

    proof

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

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

      assume that

       A1: a = A and

       A2: b = B;

      B in ( Domains_of T);

      then B in { C where C be Subset of T : C is condensed } by TDLAT_1:def 1;

      then

       A3: ex Q be Subset of T st Q = B & Q is condensed;

      thus a [= b implies A c= B

      proof

        assume a [= b;

        then (a "\/" b) = b by LATTICES:def 3;

        then (( Int ( Cl (A \/ B))) \/ (A \/ B)) = B by A1, A2, Th86;

        hence thesis by A3, Th58;

      end;

      assume A c= B;

      then (( Int ( Cl (A \/ B))) \/ (A \/ B)) = B by A3, Th58;

      then (a "\/" b) = b by A1, A2, Th86;

      hence thesis by LATTICES:def 3;

    end;

    theorem :: TDLAT_2:90

    

     Th89: for X be Subset of ( Domains_Lattice T) holds ex a be Element of ( Domains_Lattice T) st X is_less_than a & for b be Element of ( Domains_Lattice T) st X is_less_than b holds a [= b

    proof

      let X be Subset of ( Domains_Lattice T);

      X c= the carrier of ( Domains_Lattice T);

      then

       A1: X c= ( Domains_of T) by Th85;

      then

      reconsider F = X as Subset-Family of T by TOPS_2: 2;

      set A = (( union F) \/ ( Int ( Cl ( union F))));

      

       A2: F is domains-family by A1, Th64;

      then A is condensed by Th67;

      then A in { C where C be Subset of T : C is condensed };

      then

       A3: A in ( Domains_of T) by TDLAT_1:def 1;

      then

      reconsider a = A as Element of ( Domains_Lattice T) by Th85;

      

       A4: for b be Element of ( Domains_Lattice T) st X is_less_than b holds a [= b

      proof

        let b be Element of ( Domains_Lattice T);

        reconsider B = b as Element of ( Domains_of T) by Th85;

        assume

         A5: X is_less_than b;

        

         A6: for C be Subset of T st C in F holds C c= B

        proof

          let C be Subset of T;

          reconsider C1 = C as Subset of T;

          assume

           A7: C in F;

          then C1 is condensed by A2;

          then C in { P where P be Subset of T : P is condensed };

          then

           A8: C in ( Domains_of T) by TDLAT_1:def 1;

          then

          reconsider c = C as Element of ( Domains_Lattice T) by Th85;

          c [= b by A5, A7;

          hence thesis by A8, Th88;

        end;

        B in ( Domains_of T);

        then B in { C where C be Subset of T : C is condensed } by TDLAT_1:def 1;

        then ex C be Subset of T st C = B & C is condensed;

        then A c= B by A6, Th68;

        hence thesis by A3, Th88;

      end;

      take a;

      X is_less_than a

      proof

        let b be Element of ( Domains_Lattice T);

        reconsider B = b as Element of ( Domains_of T) by Th85;

        assume b in X;

        then B c= A by Th68;

        hence thesis by A3, Th88;

      end;

      hence thesis by A4;

    end;

    theorem :: TDLAT_2:91

    

     Th90: ( Domains_Lattice T) is complete

    proof

      thus for X be set holds ex a be Element of ( Domains_Lattice T) st X is_less_than a & for b be Element of ( Domains_Lattice T) st X is_less_than b holds a [= b

      proof

        let X be set;

        set Y = { c where c be Element of ( Domains_Lattice T) : c in X };

        

         A1: for d be Element of ( Domains_Lattice T) holds Y is_less_than d implies X is_less_than d

        proof

          let d be Element of ( Domains_Lattice T);

          assume

           A2: Y is_less_than d;

          thus for e be Element of ( Domains_Lattice T) st e in X holds e [= d

          proof

            let e be Element of ( Domains_Lattice T);

            assume e in X;

            then e in Y;

            hence thesis by A2;

          end;

        end;

        

         A3: for d be Element of ( Domains_Lattice T) holds X is_less_than d implies Y is_less_than d

        proof

          let d be Element of ( Domains_Lattice T);

          assume

           A4: X is_less_than d;

          thus for e be Element of ( Domains_Lattice T) st e in Y holds e [= d

          proof

            let e be Element of ( Domains_Lattice T);

            assume e in Y;

            then ex e0 be Element of ( Domains_Lattice T) st e0 = e & e0 in X;

            hence thesis by A4;

          end;

        end;

        now

          let x be object;

          assume x in Y;

          then ex y be Element of ( Domains_Lattice T) st y = x & y in X;

          hence x in the carrier of ( Domains_Lattice T);

        end;

        then

        reconsider Y as Subset of ( Domains_Lattice T) by TARSKI:def 3;

        consider a be Element of ( Domains_Lattice T) such that

         A5: Y is_less_than a and

         A6: for b be Element of ( Domains_Lattice T) st Y is_less_than b holds a [= b by Th89;

        take a;

        for b be Element of ( Domains_Lattice T) st X is_less_than b holds a [= b by A3, A6;

        hence thesis by A1, A5;

      end;

    end;

    theorem :: TDLAT_2:92

    

     Th91: for F be Subset-Family of T st F is domains-family holds for X be Subset of ( Domains_Lattice T) st X = F holds ( "\/" (X,( Domains_Lattice T))) = (( union F) \/ ( Int ( Cl ( union F))))

    proof

      let F be Subset-Family of T;

      assume

       A1: F is domains-family;

      let X be Subset of ( Domains_Lattice T);

      assume

       A2: X = F;

      thus ( "\/" (X,( Domains_Lattice T))) = (( union F) \/ ( Int ( Cl ( union F))))

      proof

        set A = (( union F) \/ ( Int ( Cl ( union F))));

        A is condensed by A1, Th67;

        then A in { C where C be Subset of T : C is condensed };

        then

         A3: A in ( Domains_of T) by TDLAT_1:def 1;

        then

        reconsider a = A as Element of ( Domains_Lattice T) by Th85;

        

         A4: X is_less_than a

        proof

          let b be Element of ( Domains_Lattice T);

          reconsider B = b as Element of ( Domains_of T) by Th85;

          assume b in X;

          then B c= A by A2, Th68;

          hence thesis by A3, Th88;

        end;

        

         A5: for b be Element of ( Domains_Lattice T) st X is_less_than b holds a [= b

        proof

          let b be Element of ( Domains_Lattice T);

          reconsider B = b as Element of ( Domains_of T) by Th85;

          assume

           A6: X is_less_than b;

          

           A7: for C be Subset of T st C in F holds C c= B

          proof

            let C be Subset of T;

            reconsider C1 = C as Subset of T;

            assume

             A8: C in F;

            then C1 is condensed by A1;

            then C in { P where P be Subset of T : P is condensed };

            then

             A9: C in ( Domains_of T) by TDLAT_1:def 1;

            then

            reconsider c = C as Element of ( Domains_Lattice T) by Th85;

            c [= b by A2, A6, A8;

            hence thesis by A9, Th88;

          end;

          B in ( Domains_of T);

          then B in { C where C be Subset of T : C is condensed } by TDLAT_1:def 1;

          then ex C be Subset of T st C = B & C is condensed;

          then A c= B by A7, Th68;

          hence thesis by A3, Th88;

        end;

        ( Domains_Lattice T) is complete by Th90;

        hence thesis by A4, A5, LATTICE3:def 21;

      end;

    end;

    theorem :: TDLAT_2:93

    

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

    proof

      let F be Subset-Family of T;

      assume

       A1: F is domains-family;

      let X be Subset of ( Domains_Lattice T);

      assume

       A2: X = F;

      thus X <> {} implies ( "/\" (X,( Domains_Lattice T))) = (( meet F) /\ ( Cl ( Int ( meet F))))

      proof

        set A = (( meet F) /\ ( Cl ( Int ( meet F))));

        A is condensed by A1, Th69;

        then A in { C where C be Subset of T : C is condensed };

        then

         A3: A in ( Domains_of T) by TDLAT_1:def 1;

        then

        reconsider a = A as Element of ( Domains_Lattice T) by Th85;

        

         A4: a is_less_than X

        proof

          let b be Element of ( Domains_Lattice T);

          reconsider B = b as Element of ( Domains_of T) by Th85;

          assume b in X;

          then A c= B by A2, Th70;

          hence thesis by A3, Th88;

        end;

        assume

         A5: X <> {} ;

        

         A6: for b be Element of ( Domains_Lattice T) st b is_less_than X holds b [= a

        proof

          let b be Element of ( Domains_Lattice T);

          reconsider B = b as Element of ( Domains_of T) by Th85;

          assume

           A7: b is_less_than X;

          

           A8: for C be Subset of T st C in F holds B c= C

          proof

            let C be Subset of T;

            reconsider C1 = C as Subset of T;

            assume

             A9: C in F;

            then C1 is condensed by A1;

            then C in { P where P be Subset of T : P is condensed };

            then

             A10: C in ( Domains_of T) by TDLAT_1:def 1;

            then

            reconsider c = C as Element of ( Domains_Lattice T) by Th85;

            b [= c by A2, A7, A9;

            hence thesis by A10, Th88;

          end;

          B in ( Domains_of T);

          then B in { C where C be Subset of T : C is condensed } by TDLAT_1:def 1;

          then ex C be Subset of T st C = B & C is condensed;

          then B c= A by A2, A5, A8, Th70;

          hence thesis by A3, Th88;

        end;

        ( Domains_Lattice T) is complete by Th90;

        hence thesis by A4, A6, LATTICE3: 34;

      end;

      thus X = {} implies ( "/\" (X,( Domains_Lattice T))) = ( [#] T)

      proof

        set A = ( [#] T);

        A is condensed by TDLAT_1: 15;

        then A in { C where C be Subset of T : C is condensed };

        then

         A11: A in ( Domains_of T) by TDLAT_1:def 1;

        then

        reconsider a = A as Element of ( Domains_Lattice T) by Th85;

        

         A12: for b be Element of ( Domains_Lattice T) st b is_less_than X holds b [= a

        proof

          let b be Element of ( Domains_Lattice T);

          reconsider B = b as Element of ( Domains_of T) by Th85;

          assume b is_less_than X;

          B c= A;

          hence thesis by A11, Th88;

        end;

        assume

         A13: X = {} ;

        

         A14: a is_less_than X by A13;

        ( Domains_Lattice T) is complete by Th90;

        hence thesis by A14, A12, LATTICE3: 34;

      end;

    end;

    begin

    reserve T for non empty TopSpace;

    theorem :: TDLAT_2:94

    

     Th93: the carrier of ( Closed_Domains_Lattice T) = ( Closed_Domains_of T)

    proof

      ( Closed_Domains_Lattice T) = LattStr (# ( Closed_Domains_of T), ( CLD-Union T), ( CLD-Meet T) #) by TDLAT_1:def 8;

      hence thesis;

    end;

    theorem :: TDLAT_2:95

    

     Th94: for a,b be Element of ( Closed_Domains_Lattice T) holds for A,B be Element of ( Closed_Domains_of T) st a = A & b = B holds (a "\/" b) = (A \/ B) & (a "/\" b) = ( Cl ( Int (A /\ B)))

    proof

      let a,b be Element of ( Closed_Domains_Lattice T);

      let A,B be Element of ( Closed_Domains_of T);

      assume that

       A1: a = A and

       A2: b = B;

      

       A3: ( Closed_Domains_Lattice T) = LattStr (# ( Closed_Domains_of T), ( CLD-Union T), ( CLD-Meet T) #) by TDLAT_1:def 8;

      

      hence (a "\/" b) = (( CLD-Union T) . (A,B)) by A1, A2, LATTICES:def 1

      .= (A \/ B) by TDLAT_1:def 6;

      

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

      .= ( Cl ( Int (A /\ B))) by TDLAT_1:def 7;

    end;

    theorem :: TDLAT_2:96

    ( Bottom ( Closed_Domains_Lattice T)) = ( {} T) & ( Top ( Closed_Domains_Lattice T)) = ( [#] T)

    proof

      thus ( Bottom ( Closed_Domains_Lattice T)) = ( {} T)

      proof

        ( {} T) is closed_condensed by TDLAT_1: 18;

        then

         A1: ( {} T) in { A where A be Subset of T : A is closed_condensed };

        then

        reconsider E = ( {} T) as Element of ( Closed_Domains_of T) by TDLAT_1:def 5;

        ( {} T) in ( Closed_Domains_of T) by A1, TDLAT_1:def 5;

        then

        reconsider e = ( {} T) as Element of ( Closed_Domains_Lattice T) by Th93;

        for a be Element of ( Closed_Domains_Lattice T) holds (e "\/" a) = a

        proof

          let a be Element of ( Closed_Domains_Lattice T);

          reconsider A = a as Element of ( Closed_Domains_of T) by Th93;

          

          thus (e "\/" a) = (E \/ A) by Th94

          .= a;

        end;

        hence thesis by LATTICE2: 14;

      end;

      thus ( Top ( Closed_Domains_Lattice T)) = ( [#] T)

      proof

        ( [#] T) is closed_condensed by TDLAT_1: 19;

        then

         A2: ( [#] T) in { A where A be Subset of T : A is closed_condensed };

        then

        reconsider E = ( [#] T) as Element of ( Closed_Domains_of T) by TDLAT_1:def 5;

        ( [#] T) in ( Closed_Domains_of T) by A2, TDLAT_1:def 5;

        then

        reconsider e = ( [#] T) as Element of ( Closed_Domains_Lattice T) by Th93;

        for a be Element of ( Closed_Domains_Lattice T) holds (e "/\" a) = a

        proof

          let a be Element of ( Closed_Domains_Lattice T);

          reconsider A = a as Element of ( Closed_Domains_of T) by Th93;

          A in ( Closed_Domains_of T);

          then A in { C where C be Subset of T : C is closed_condensed } by TDLAT_1:def 5;

          then

           A3: ex D be Subset of T st D = A & D is closed_condensed;

          

          thus (e "/\" a) = ( Cl ( Int (E /\ A))) by Th94

          .= ( Cl ( Int A)) by XBOOLE_1: 28

          .= a by A3, TOPS_1:def 7;

        end;

        hence thesis by LATTICE2: 16;

      end;

    end;

    theorem :: TDLAT_2:97

    

     Th96: for a,b be Element of ( Closed_Domains_Lattice T) holds for A,B be Element of ( Closed_Domains_of T) st a = A & b = B holds a [= b iff A c= B

    proof

      let a,b be Element of ( Closed_Domains_Lattice T);

      let A,B be Element of ( Closed_Domains_of T);

      assume that

       A1: a = A and

       A2: b = B;

      thus a [= b implies A c= B

      proof

        assume a [= b;

        then (a "\/" b) = b by LATTICES:def 3;

        then (A \/ B) = B by A1, A2, Th94;

        hence thesis by XBOOLE_1: 7;

      end;

      thus A c= B implies a [= b

      proof

        assume A c= B;

        then (A \/ B) = B by XBOOLE_1: 12;

        then (a "\/" b) = b by A1, A2, Th94;

        hence thesis by LATTICES:def 3;

      end;

    end;

    theorem :: TDLAT_2:98

    

     Th97: for X be Subset of ( Closed_Domains_Lattice T) holds ex a be Element of ( Closed_Domains_Lattice T) st X is_less_than a & for b be Element of ( Closed_Domains_Lattice T) st X is_less_than b holds a [= b

    proof

      let X be Subset of ( Closed_Domains_Lattice T);

      X c= the carrier of ( Closed_Domains_Lattice T);

      then

       A1: X c= ( Closed_Domains_of T) by Th93;

      then

      reconsider F = X as Subset-Family of T by TOPS_2: 2;

      set A = ( Cl ( union F));

      

       A2: F is closed-domains-family by A1, Th71;

      then A is closed_condensed by Th75;

      then A in { C where C be Subset of T : C is closed_condensed };

      then

       A3: A in ( Closed_Domains_of T) by TDLAT_1:def 5;

      then

      reconsider a = A as Element of ( Closed_Domains_Lattice T) by Th93;

      

       A4: for b be Element of ( Closed_Domains_Lattice T) st X is_less_than b holds a [= b

      proof

        let b be Element of ( Closed_Domains_Lattice T);

        reconsider B = b as Element of ( Closed_Domains_of T) by Th93;

        assume

         A5: X is_less_than b;

        

         A6: for C be Subset of T st C in F holds C c= B

        proof

          let C be Subset of T;

          reconsider C1 = C as Subset of T;

          assume

           A7: C in F;

          then C1 is closed_condensed by A2;

          then C in { P where P be Subset of T : P is closed_condensed };

          then

           A8: C in ( Closed_Domains_of T) by TDLAT_1:def 5;

          then

          reconsider c = C as Element of ( Closed_Domains_Lattice T) by Th93;

          c [= b by A5, A7;

          hence thesis by A8, Th96;

        end;

        B in ( Closed_Domains_of T);

        then B in { C where C be Subset of T : C is closed_condensed } by TDLAT_1:def 5;

        then ex C be Subset of T st C = B & C is closed_condensed;

        then A c= B by A6, Th76;

        hence thesis by A3, Th96;

      end;

      take a;

      X is_less_than a

      proof

        let b be Element of ( Closed_Domains_Lattice T);

        reconsider B = b as Element of ( Closed_Domains_of T) by Th93;

        assume b in X;

        then B c= A by Th76;

        hence thesis by A3, Th96;

      end;

      hence thesis by A4;

    end;

    theorem :: TDLAT_2:99

    

     Th98: ( Closed_Domains_Lattice T) is complete

    proof

      thus for X be set holds ex a be Element of ( Closed_Domains_Lattice T) st X is_less_than a & for b be Element of ( Closed_Domains_Lattice T) st X is_less_than b holds a [= b

      proof

        let X be set;

        set Y = { c where c be Element of ( Closed_Domains_Lattice T) : c in X };

        

         A1: for d be Element of ( Closed_Domains_Lattice T) holds Y is_less_than d implies X is_less_than d

        proof

          let d be Element of ( Closed_Domains_Lattice T);

          assume

           A2: Y is_less_than d;

          thus for e be Element of ( Closed_Domains_Lattice T) st e in X holds e [= d

          proof

            let e be Element of ( Closed_Domains_Lattice T);

            assume e in X;

            then e in Y;

            hence thesis by A2;

          end;

        end;

        

         A3: for d be Element of ( Closed_Domains_Lattice T) holds X is_less_than d implies Y is_less_than d

        proof

          let d be Element of ( Closed_Domains_Lattice T);

          assume

           A4: X is_less_than d;

          thus for e be Element of ( Closed_Domains_Lattice T) st e in Y holds e [= d

          proof

            let e be Element of ( Closed_Domains_Lattice T);

            assume e in Y;

            then ex e0 be Element of ( Closed_Domains_Lattice T) st e0 = e & e0 in X;

            hence thesis by A4;

          end;

        end;

        now

          let x be object;

          assume x in Y;

          then ex y be Element of ( Closed_Domains_Lattice T) st y = x & y in X;

          hence x in the carrier of ( Closed_Domains_Lattice T);

        end;

        then

        reconsider Y as Subset of ( Closed_Domains_Lattice T) by TARSKI:def 3;

        consider a be Element of ( Closed_Domains_Lattice T) such that

         A5: Y is_less_than a and

         A6: for b be Element of ( Closed_Domains_Lattice T) st Y is_less_than b holds a [= b by Th97;

        take a;

        for b be Element of ( Closed_Domains_Lattice T) st X is_less_than b holds a [= b by A3, A6;

        hence thesis by A1, A5;

      end;

    end;

    theorem :: TDLAT_2:100

    for F be Subset-Family of T st F is closed-domains-family holds for X be Subset of ( Closed_Domains_Lattice T) st X = F holds ( "\/" (X,( Closed_Domains_Lattice T))) = ( Cl ( union F))

    proof

      let F be Subset-Family of T;

      assume

       A1: F is closed-domains-family;

      let X be Subset of ( Closed_Domains_Lattice T);

      assume

       A2: X = F;

      thus ( "\/" (X,( Closed_Domains_Lattice T))) = ( Cl ( union F))

      proof

        set A = ( Cl ( union F));

        A is closed_condensed by A1, Th75;

        then A in { C where C be Subset of T : C is closed_condensed };

        then

         A3: A in ( Closed_Domains_of T) by TDLAT_1:def 5;

        then

        reconsider a = A as Element of ( Closed_Domains_Lattice T) by Th93;

        

         A4: X is_less_than a

        proof

          let b be Element of ( Closed_Domains_Lattice T);

          reconsider B = b as Element of ( Closed_Domains_of T) by Th93;

          assume b in X;

          then B c= A by A2, Th76;

          hence thesis by A3, Th96;

        end;

        

         A5: for b be Element of ( Closed_Domains_Lattice T) st X is_less_than b holds a [= b

        proof

          let b be Element of ( Closed_Domains_Lattice T);

          reconsider B = b as Element of ( Closed_Domains_of T) by Th93;

          assume

           A6: X is_less_than b;

          

           A7: for C be Subset of T st C in F holds C c= B

          proof

            let C be Subset of T;

            reconsider C1 = C as Subset of T;

            assume

             A8: C in F;

            then C1 is closed_condensed by A1;

            then C in { P where P be Subset of T : P is closed_condensed };

            then

             A9: C in ( Closed_Domains_of T) by TDLAT_1:def 5;

            then

            reconsider c = C as Element of ( Closed_Domains_Lattice T) by Th93;

            c [= b by A2, A6, A8;

            hence thesis by A9, Th96;

          end;

          B in ( Closed_Domains_of T);

          then B in { C where C be Subset of T : C is closed_condensed } by TDLAT_1:def 5;

          then ex C be Subset of T st C = B & C is closed_condensed;

          then A c= B by A7, Th76;

          hence thesis by A3, Th96;

        end;

        ( Closed_Domains_Lattice T) is complete by Th98;

        hence thesis by A4, A5, LATTICE3:def 21;

      end;

    end;

    theorem :: TDLAT_2:101

    for F be Subset-Family of T st F is closed-domains-family holds for X be Subset of ( Closed_Domains_Lattice T) st X = F holds (X <> {} implies ( "/\" (X,( Closed_Domains_Lattice T))) = ( Cl ( Int ( meet F)))) & (X = {} implies ( "/\" (X,( Closed_Domains_Lattice T))) = ( [#] T))

    proof

      let F be Subset-Family of T;

      assume

       A1: F is closed-domains-family;

      let X be Subset of ( Closed_Domains_Lattice T);

      assume

       A2: X = F;

      thus X <> {} implies ( "/\" (X,( Closed_Domains_Lattice T))) = ( Cl ( Int ( meet F)))

      proof

        set A = ( Cl ( Int ( meet F)));

        A is closed_condensed by A1, Th75;

        then A in { C where C be Subset of T : C is closed_condensed };

        then

         A3: A in ( Closed_Domains_of T) by TDLAT_1:def 5;

        then

        reconsider a = A as Element of ( Closed_Domains_Lattice T) by Th93;

        

         A4: a is_less_than X

        proof

          let b be Element of ( Closed_Domains_Lattice T);

          reconsider B = b as Element of ( Closed_Domains_of T) by Th93;

          assume b in X;

          then A c= B by A1, A2, Th73, Th77;

          hence thesis by A3, Th96;

        end;

        assume

         A5: X <> {} ;

        

         A6: for b be Element of ( Closed_Domains_Lattice T) st b is_less_than X holds b [= a

        proof

          let b be Element of ( Closed_Domains_Lattice T);

          reconsider B = b as Element of ( Closed_Domains_of T) by Th93;

          assume

           A7: b is_less_than X;

          

           A8: for C be Subset of T st C in F holds B c= C

          proof

            let C be Subset of T;

            reconsider C1 = C as Subset of T;

            assume

             A9: C in F;

            then C1 is closed_condensed by A1;

            then C in { P where P be Subset of T : P is closed_condensed };

            then

             A10: C in ( Closed_Domains_of T) by TDLAT_1:def 5;

            then

            reconsider c = C as Element of ( Closed_Domains_Lattice T) by Th93;

            b [= c by A2, A7, A9;

            hence thesis by A10, Th96;

          end;

          B in ( Closed_Domains_of T);

          then B in { C where C be Subset of T : C is closed_condensed } by TDLAT_1:def 5;

          then ex C be Subset of T st C = B & C is closed_condensed;

          then B c= A by A2, A5, A8, Th77;

          hence thesis by A3, Th96;

        end;

        ( Closed_Domains_Lattice T) is complete by Th98;

        hence thesis by A4, A6, LATTICE3: 34;

      end;

      thus X = {} implies ( "/\" (X,( Closed_Domains_Lattice T))) = ( [#] T)

      proof

        set A = ( [#] T);

        A is closed_condensed by TDLAT_1: 19;

        then A in { C where C be Subset of T : C is closed_condensed };

        then

         A11: A in ( Closed_Domains_of T) by TDLAT_1:def 5;

        then

        reconsider a = A as Element of ( Closed_Domains_Lattice T) by Th93;

        

         A12: for b be Element of ( Closed_Domains_Lattice T) st b is_less_than X holds b [= a

        proof

          let b be Element of ( Closed_Domains_Lattice T);

          reconsider B = b as Element of ( Closed_Domains_of T) by Th93;

          assume b is_less_than X;

          B c= A;

          hence thesis by A11, Th96;

        end;

        assume

         A13: X = {} ;

        

         A14: a is_less_than X by A13;

        ( Closed_Domains_Lattice T) is complete by Th98;

        hence thesis by A14, A12, LATTICE3: 34;

      end;

    end;

    theorem :: TDLAT_2:102

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

    proof

      let F be Subset-Family of T;

      

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

      assume

       A2: F is closed-domains-family;

      then

       A3: F is domains-family by Th72;

      let X be Subset of ( Domains_Lattice T);

      assume

       A4: X = F;

      ( meet F) is closed by A2, Th73, TOPS_2: 22;

      then ( Cl ( Int ( meet F))) c= ( meet F) by A1, PRE_TOPC: 22;

      then (( meet F) /\ ( Cl ( Int ( meet F)))) = ( Cl ( Int ( meet F))) by XBOOLE_1: 28;

      hence X <> {} implies ( "/\" (X,( Domains_Lattice T))) = ( Cl ( Int ( meet F))) by A3, A4, Th92;

      thus thesis by A3, A4, Th92;

    end;

    theorem :: TDLAT_2:103

    

     Th102: the carrier of ( Open_Domains_Lattice T) = ( Open_Domains_of T)

    proof

      ( Open_Domains_Lattice T) = LattStr (# ( Open_Domains_of T), ( OPD-Union T), ( OPD-Meet T) #) by TDLAT_1:def 12;

      hence thesis;

    end;

    theorem :: TDLAT_2:104

    

     Th103: for a,b be Element of ( Open_Domains_Lattice T) holds for A,B be Element of ( Open_Domains_of T) st a = A & b = B holds (a "\/" b) = ( Int ( Cl (A \/ B))) & (a "/\" b) = (A /\ B)

    proof

      let a,b be Element of ( Open_Domains_Lattice T);

      let A,B be Element of ( Open_Domains_of T);

      assume that

       A1: a = A and

       A2: b = B;

      

       A3: ( Open_Domains_Lattice T) = LattStr (# ( Open_Domains_of T), ( OPD-Union T), ( OPD-Meet T) #) by TDLAT_1:def 12;

      

      hence (a "\/" b) = (( OPD-Union T) . (A,B)) by A1, A2, LATTICES:def 1

      .= ( Int ( Cl (A \/ B))) by TDLAT_1:def 10;

      

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

      .= (A /\ B) by TDLAT_1:def 11;

    end;

    theorem :: TDLAT_2:105

    ( Bottom ( Open_Domains_Lattice T)) = ( {} T) & ( Top ( Open_Domains_Lattice T)) = ( [#] T)

    proof

      thus ( Bottom ( Open_Domains_Lattice T)) = ( {} T)

      proof

        ( {} T) is open_condensed by TDLAT_1: 20;

        then

         A1: ( {} T) in { A where A be Subset of T : A is open_condensed };

        then

        reconsider E = ( {} T) as Element of ( Open_Domains_of T) by TDLAT_1:def 9;

        ( {} T) in ( Open_Domains_of T) by A1, TDLAT_1:def 9;

        then

        reconsider e = ( {} T) as Element of ( Open_Domains_Lattice T) by Th102;

        for a be Element of ( Open_Domains_Lattice T) holds (e "\/" a) = a

        proof

          let a be Element of ( Open_Domains_Lattice T);

          reconsider A = a as Element of ( Open_Domains_of T) by Th102;

          A in ( Open_Domains_of T);

          then A in { C where C be Subset of T : C is open_condensed } by TDLAT_1:def 9;

          then

           A2: ex D be Subset of T st D = A & D is open_condensed;

          

          thus (e "\/" a) = ( Int ( Cl (E \/ A))) by Th103

          .= a by A2, TOPS_1:def 8;

        end;

        hence thesis by LATTICE2: 14;

      end;

      thus ( Top ( Open_Domains_Lattice T)) = ( [#] T)

      proof

        ( [#] T) is open_condensed by TDLAT_1: 21;

        then

         A3: ( [#] T) in { A where A be Subset of T : A is open_condensed };

        then

        reconsider E = ( [#] T) as Element of ( Open_Domains_of T) by TDLAT_1:def 9;

        ( [#] T) in ( Open_Domains_of T) by A3, TDLAT_1:def 9;

        then

        reconsider e = ( [#] T) as Element of ( Open_Domains_Lattice T) by Th102;

        for a be Element of ( Open_Domains_Lattice T) holds (e "/\" a) = a

        proof

          let a be Element of ( Open_Domains_Lattice T);

          reconsider A = a as Element of ( Open_Domains_of T) by Th102;

          

          thus (e "/\" a) = (E /\ A) by Th103

          .= a by XBOOLE_1: 28;

        end;

        hence thesis by LATTICE2: 16;

      end;

    end;

    theorem :: TDLAT_2:106

    

     Th105: for a,b be Element of ( Open_Domains_Lattice T) holds for A,B be Element of ( Open_Domains_of T) st a = A & b = B holds a [= b iff A c= B

    proof

      let a,b be Element of ( Open_Domains_Lattice T);

      let A,B be Element of ( Open_Domains_of T);

      reconsider A1 = A as Subset of T;

      assume that

       A1: a = A and

       A2: b = B;

      A in ( Open_Domains_of T);

      then A in { C where C be Subset of T : C is open_condensed } by TDLAT_1:def 9;

      then ex Q be Subset of T st Q = A & Q is open_condensed;

      then

       A3: A1 is open by TOPS_1: 67;

      thus a [= b implies A c= B

      proof

        assume a [= b;

        then (a "\/" b) = b by LATTICES:def 3;

        then ( Int ( Cl (A \/ B))) = B by A1, A2, Th103;

        hence thesis by A3, Th4;

      end;

      B in ( Open_Domains_of T);

      then B in { C where C be Subset of T : C is open_condensed } by TDLAT_1:def 9;

      then

       A4: ex P be Subset of T st P = B & P is open_condensed;

      thus A c= B implies a [= b

      proof

        assume A c= B;

        then ( Int ( Cl (A \/ B))) = B by A4, Th63;

        then (a "\/" b) = b by A1, A2, Th103;

        hence thesis by LATTICES:def 3;

      end;

    end;

    theorem :: TDLAT_2:107

    

     Th106: for X be Subset of ( Open_Domains_Lattice T) holds ex a be Element of ( Open_Domains_Lattice T) st X is_less_than a & for b be Element of ( Open_Domains_Lattice T) st X is_less_than b holds a [= b

    proof

      let X be Subset of ( Open_Domains_Lattice T);

      X c= the carrier of ( Open_Domains_Lattice T);

      then

       A1: X c= ( Open_Domains_of T) by Th102;

      then

      reconsider F = X as Subset-Family of T by TOPS_2: 2;

      set A = ( Int ( Cl ( union F)));

      

       A2: F is open-domains-family by A1, Th78;

      then A is open_condensed by Th82;

      then A in { C where C be Subset of T : C is open_condensed };

      then

       A3: A in ( Open_Domains_of T) by TDLAT_1:def 9;

      then

      reconsider a = A as Element of ( Open_Domains_Lattice T) by Th102;

      

       A4: for b be Element of ( Open_Domains_Lattice T) st X is_less_than b holds a [= b

      proof

        let b be Element of ( Open_Domains_Lattice T);

        reconsider B = b as Element of ( Open_Domains_of T) by Th102;

        assume

         A5: X is_less_than b;

        

         A6: for C be Subset of T st C in F holds C c= B

        proof

          let C be Subset of T;

          reconsider C1 = C as Subset of T;

          assume

           A7: C in F;

          then C1 is open_condensed by A2;

          then C in { P where P be Subset of T : P is open_condensed };

          then

           A8: C in ( Open_Domains_of T) by TDLAT_1:def 9;

          then

          reconsider c = C as Element of ( Open_Domains_Lattice T) by Th102;

          c [= b by A5, A7;

          hence thesis by A8, Th105;

        end;

        B in ( Open_Domains_of T);

        then B in { C where C be Subset of T : C is open_condensed } by TDLAT_1:def 9;

        then ex C be Subset of T st C = B & C is open_condensed;

        then A c= B by A6, Th83;

        hence thesis by A3, Th105;

      end;

      take a;

      X is_less_than a

      proof

        let b be Element of ( Open_Domains_Lattice T);

        reconsider B = b as Element of ( Open_Domains_of T) by Th102;

        assume b in X;

        then B c= A by A2, Th80, Th83;

        hence thesis by A3, Th105;

      end;

      hence thesis by A4;

    end;

    theorem :: TDLAT_2:108

    

     Th107: ( Open_Domains_Lattice T) is complete

    proof

      thus for X be set holds ex a be Element of ( Open_Domains_Lattice T) st X is_less_than a & for b be Element of ( Open_Domains_Lattice T) st X is_less_than b holds a [= b

      proof

        let X be set;

        set Y = { c where c be Element of ( Open_Domains_Lattice T) : c in X };

        

         A1: for d be Element of ( Open_Domains_Lattice T) holds Y is_less_than d implies X is_less_than d

        proof

          let d be Element of ( Open_Domains_Lattice T);

          assume

           A2: Y is_less_than d;

          thus for e be Element of ( Open_Domains_Lattice T) st e in X holds e [= d

          proof

            let e be Element of ( Open_Domains_Lattice T);

            assume e in X;

            then e in Y;

            hence thesis by A2;

          end;

        end;

        

         A3: for d be Element of ( Open_Domains_Lattice T) holds X is_less_than d implies Y is_less_than d

        proof

          let d be Element of ( Open_Domains_Lattice T);

          assume

           A4: X is_less_than d;

          thus for e be Element of ( Open_Domains_Lattice T) st e in Y holds e [= d

          proof

            let e be Element of ( Open_Domains_Lattice T);

            assume e in Y;

            then ex e0 be Element of ( Open_Domains_Lattice T) st e0 = e & e0 in X;

            hence thesis by A4;

          end;

        end;

        now

          let x be object;

          assume x in Y;

          then ex y be Element of ( Open_Domains_Lattice T) st y = x & y in X;

          hence x in the carrier of ( Open_Domains_Lattice T);

        end;

        then

        reconsider Y as Subset of ( Open_Domains_Lattice T) by TARSKI:def 3;

        consider a be Element of ( Open_Domains_Lattice T) such that

         A5: Y is_less_than a and

         A6: for b be Element of ( Open_Domains_Lattice T) st Y is_less_than b holds a [= b by Th106;

        take a;

        for b be Element of ( Open_Domains_Lattice T) st X is_less_than b holds a [= b by A3, A6;

        hence thesis by A1, A5;

      end;

    end;

    theorem :: TDLAT_2:109

    for F be Subset-Family of T st F is open-domains-family holds for X be Subset of ( Open_Domains_Lattice T) st X = F holds ( "\/" (X,( Open_Domains_Lattice T))) = ( Int ( Cl ( union F)))

    proof

      let F be Subset-Family of T;

      assume

       A1: F is open-domains-family;

      let X be Subset of ( Open_Domains_Lattice T);

      assume

       A2: X = F;

      thus ( "\/" (X,( Open_Domains_Lattice T))) = ( Int ( Cl ( union F)))

      proof

        set A = ( Int ( Cl ( union F)));

        A is open_condensed by A1, Th82;

        then A in { C where C be Subset of T : C is open_condensed };

        then

         A3: A in ( Open_Domains_of T) by TDLAT_1:def 9;

        then

        reconsider a = A as Element of ( Open_Domains_Lattice T) by Th102;

        

         A4: X is_less_than a

        proof

          let b be Element of ( Open_Domains_Lattice T);

          reconsider B = b as Element of ( Open_Domains_of T) by Th102;

          assume b in X;

          then B c= A by A1, A2, Th80, Th83;

          hence thesis by A3, Th105;

        end;

        

         A5: for b be Element of ( Open_Domains_Lattice T) st X is_less_than b holds a [= b

        proof

          let b be Element of ( Open_Domains_Lattice T);

          reconsider B = b as Element of ( Open_Domains_of T) by Th102;

          assume

           A6: X is_less_than b;

          

           A7: for C be Subset of T st C in F holds C c= B

          proof

            let C be Subset of T;

            reconsider C1 = C as Subset of T;

            assume

             A8: C in F;

            then C1 is open_condensed by A1;

            then C in { P where P be Subset of T : P is open_condensed };

            then

             A9: C in ( Open_Domains_of T) by TDLAT_1:def 9;

            then

            reconsider c = C as Element of ( Open_Domains_Lattice T) by Th102;

            c [= b by A2, A6, A8;

            hence thesis by A9, Th105;

          end;

          B in ( Open_Domains_of T);

          then B in { C where C be Subset of T : C is open_condensed } by TDLAT_1:def 9;

          then ex C be Subset of T st C = B & C is open_condensed;

          then A c= B by A7, Th83;

          hence thesis by A3, Th105;

        end;

        ( Open_Domains_Lattice T) is complete by Th107;

        hence thesis by A4, A5, LATTICE3:def 21;

      end;

    end;

    theorem :: TDLAT_2:110

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

    proof

      let F be Subset-Family of T;

      assume

       A1: F is open-domains-family;

      let X be Subset of ( Open_Domains_Lattice T);

      assume

       A2: X = F;

      thus X <> {} implies ( "/\" (X,( Open_Domains_Lattice T))) = ( Int ( meet F))

      proof

        set A = ( Int ( meet F));

        A is open_condensed by A1, Th82;

        then A in { C where C be Subset of T : C is open_condensed };

        then

         A3: A in ( Open_Domains_of T) by TDLAT_1:def 9;

        then

        reconsider a = A as Element of ( Open_Domains_Lattice T) by Th102;

        

         A4: a is_less_than X

        proof

          let b be Element of ( Open_Domains_Lattice T);

          reconsider B = b as Element of ( Open_Domains_of T) by Th102;

          assume b in X;

          then A c= B by A2, Th84;

          hence thesis by A3, Th105;

        end;

        assume

         A5: X <> {} ;

        

         A6: for b be Element of ( Open_Domains_Lattice T) st b is_less_than X holds b [= a

        proof

          let b be Element of ( Open_Domains_Lattice T);

          reconsider B = b as Element of ( Open_Domains_of T) by Th102;

          assume

           A7: b is_less_than X;

          

           A8: for C be Subset of T st C in F holds B c= C

          proof

            let C be Subset of T;

            reconsider C1 = C as Subset of T;

            assume

             A9: C in F;

            then C1 is open_condensed by A1;

            then C in { P where P be Subset of T : P is open_condensed };

            then

             A10: C in ( Open_Domains_of T) by TDLAT_1:def 9;

            then

            reconsider c = C as Element of ( Open_Domains_Lattice T) by Th102;

            b [= c by A2, A7, A9;

            hence thesis by A10, Th105;

          end;

          B in ( Open_Domains_of T);

          then B in { C where C be Subset of T : C is open_condensed } by TDLAT_1:def 9;

          then ex C be Subset of T st C = B & C is open_condensed;

          then B c= A by A2, A5, A8, Th84;

          hence thesis by A3, Th105;

        end;

        ( Open_Domains_Lattice T) is complete by Th107;

        hence thesis by A4, A6, LATTICE3: 34;

      end;

      thus X = {} implies ( "/\" (X,( Open_Domains_Lattice T))) = ( [#] T)

      proof

        set A = ( [#] T);

        A is open_condensed by TDLAT_1: 21;

        then A in { C where C be Subset of T : C is open_condensed };

        then

         A11: A in ( Open_Domains_of T) by TDLAT_1:def 9;

        then

        reconsider a = A as Element of ( Open_Domains_Lattice T) by Th102;

        

         A12: for b be Element of ( Open_Domains_Lattice T) st b is_less_than X holds b [= a

        proof

          let b be Element of ( Open_Domains_Lattice T);

          reconsider B = b as Element of ( Open_Domains_of T) by Th102;

          assume b is_less_than X;

          B c= A;

          hence thesis by A11, Th105;

        end;

        assume

         A13: X = {} ;

        

         A14: a is_less_than X by A13;

        ( Open_Domains_Lattice T) is complete by Th107;

        hence thesis by A14, A12, LATTICE3: 34;

      end;

    end;

    theorem :: TDLAT_2:111

    for F be Subset-Family of T st F is open-domains-family holds for X be Subset of ( Domains_Lattice T) st X = F holds ( "\/" (X,( Domains_Lattice T))) = ( Int ( Cl ( union F)))

    proof

      let F be Subset-Family of T;

      

       A1: ( Int ( union F)) c= ( Int ( Cl ( union F))) by PRE_TOPC: 18, TOPS_1: 19;

      assume

       A2: F is open-domains-family;

      then ( union F) is open by Th80, TOPS_2: 19;

      then ( union F) c= ( Int ( Cl ( union F))) by A1, TOPS_1: 23;

      then

       A3: (( union F) \/ ( Int ( Cl ( union F)))) = ( Int ( Cl ( union F))) by XBOOLE_1: 12;

      let X be Subset of ( Domains_Lattice T);

      assume X = F;

      hence thesis by A2, A3, Th79, Th91;

    end;