tdlat_1.miz



    begin

    reserve T for 1-sorted;

    theorem :: TDLAT_1:1

    

     Th1: for A,B be Subset of T holds (A \/ B) = ( [#] T) iff (A ` ) c= B

    proof

      let A,B be Subset of T;

      hereby

        assume (A \/ B) = ( [#] T);

        then (( [#] T) \ A) = (B \ A) by XBOOLE_1: 40;

        hence (A ` ) c= B by XBOOLE_1: 36;

      end;

      assume (A ` ) c= B;

      then (A \/ (A ` )) c= (A \/ B) by XBOOLE_1: 9;

      then ( [#] T) c= (A \/ B) by PRE_TOPC: 2;

      hence (A \/ B) = ( [#] T);

    end;

    theorem :: TDLAT_1:2

    

     Th2: for A,B be Subset of T holds A misses B iff B c= (A ` ) by SUBSET_1: 23;

    reserve T for TopSpace;

    theorem :: TDLAT_1:3

    

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

    proof

      let A be Subset of T;

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

      hence thesis;

    end;

    theorem :: TDLAT_1:4

    

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

    proof

      let A be Subset of T;

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

      hence thesis;

    end;

    theorem :: TDLAT_1:5

    

     Th5: for A be Subset of T holds ( Int ( Cl A)) = ( Int ( Cl ( Int ( Cl A))))

    proof

      let A be Subset of T;

      

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

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

      hence thesis by A1;

    end;

    theorem :: TDLAT_1:6

    

     Th6: for A,B be Subset of T st A is closed or B is closed holds (( Cl ( Int A)) \/ ( Cl ( Int B))) = ( Cl ( Int (A \/ B)))

    proof

      let A,B be Subset of T;

      

       A1: ((A \/ B) \/ ((A \/ B) ` )) c= ((A \/ B) \/ ( Cl ((A \/ B) ` ))) by PRE_TOPC: 18, XBOOLE_1: 9;

      ((A \/ B) \/ ((A \/ B) ` )) = ( [#] T) by PRE_TOPC: 2;

      then

       A2: ((A \/ B) \/ ( Cl ((A \/ B) ` ))) = ( [#] T) by A1;

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

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

      then

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

      (B \/ (A \/ ( Cl ((A \/ B) ` )))) = ( [#] T) by A2, XBOOLE_1: 4;

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

      then

       A4: ( Cl (B ` )) c= ( Cl (A \/ ( Cl ((A \/ B) ` )))) by PRE_TOPC: 19;

      assume

       A5: A is closed or B is closed;

       A6:

      now

        per cases by A5;

          suppose A is closed;

          then ((( Cl (B ` )) ` ) ` ) c= (A \/ ( Cl ((B \/ A) ` ))) by A4, PRE_TOPC: 22;

          then ((( Cl (B ` )) ` ) \/ (A \/ ( Cl ((B \/ A) ` )))) = ( [#] T) by Th1;

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

          then (A \/ (( Int B) \/ ( Cl ((B \/ A) ` )))) = ( [#] T) by XBOOLE_1: 4;

          then (A ` ) c= (( Int B) \/ ( Cl ((B \/ A) ` ))) by Th1;

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

          then ( Cl (A ` )) c= (( Cl ( Int B)) \/ ( Cl ( Cl ((B \/ A) ` )))) by PRE_TOPC: 20;

          then (( Cl (A ` )) \/ (( Cl (A ` )) ` )) c= ((( Cl ( Int B)) \/ ( Cl ((B \/ A) ` ))) \/ (( Cl (A ` )) ` )) by XBOOLE_1: 9;

          then ( [#] T) c= ((( Cl ( Int B)) \/ ( Cl ((B \/ A) ` ))) \/ (( Cl (A ` )) ` )) by PRE_TOPC: 2;

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

          then ( [#] T) c= (( Cl ((B \/ A) ` )) \/ (( Cl ( Int B)) \/ ( Int A))) by XBOOLE_1: 4;

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

          then (( Cl ((B \/ A) ` )) ` ) c= (( Cl ( Int B)) \/ ( Int A)) by Th1;

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

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

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

          hence ( Cl ( Int (A \/ B))) c= (( Cl ( Int A)) \/ ( Cl ( Int B)));

        end;

          suppose B is closed;

          then ((( Cl (A ` )) ` ) ` ) c= (B \/ ( Cl ((A \/ B) ` ))) by A3, PRE_TOPC: 22;

          then ((( Cl (A ` )) ` ) \/ (B \/ ( Cl ((A \/ B) ` )))) = ( [#] T) by Th1;

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

          then (B \/ (( Int A) \/ ( Cl ((A \/ B) ` )))) = ( [#] T) by XBOOLE_1: 4;

          then (B ` ) c= (( Int A) \/ ( Cl ((A \/ B) ` ))) by Th1;

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

          then ( Cl (B ` )) c= (( Cl ( Int A)) \/ ( Cl ( Cl ((A \/ B) ` )))) by PRE_TOPC: 20;

          then (( Cl (B ` )) \/ (( Cl (B ` )) ` )) c= ((( Cl ( Int A)) \/ ( Cl ((A \/ B) ` ))) \/ (( Cl (B ` )) ` )) by XBOOLE_1: 9;

          then ( [#] T) c= ((( Cl ( Int A)) \/ ( Cl ((A \/ B) ` ))) \/ (( Cl (B ` )) ` )) by PRE_TOPC: 2;

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

          then ( [#] T) c= (( Cl ((A \/ B) ` )) \/ (( Cl ( Int A)) \/ ( Int B))) by XBOOLE_1: 4;

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

          then (( Cl ((A \/ B) ` )) ` ) c= (( Cl ( Int A)) \/ ( Int B)) by Th1;

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

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

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

          hence ( Cl ( Int (A \/ B))) c= (( Cl ( Int A)) \/ ( Cl ( Int B)));

        end;

      end;

      ( Int B) c= ( Int (A \/ B)) by TOPS_1: 19, XBOOLE_1: 7;

      then

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

      ( Int A) c= ( Int (A \/ B)) by TOPS_1: 19, XBOOLE_1: 7;

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

      then (( Cl ( Int A)) \/ ( Cl ( Int B))) c= ( Cl ( Int (A \/ B))) by A7, XBOOLE_1: 8;

      hence thesis by A6;

    end;

    theorem :: TDLAT_1:7

    

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

    proof

      let A,B be Subset of T;

      

       A1: ( Int (A ` )) misses (( Int (A ` )) ` ) by XBOOLE_1: 79;

      

       A2: ( Int (B ` )) misses (( Int (B ` )) ` ) by XBOOLE_1: 79;

      (A /\ B) misses ((A /\ B) ` ) by XBOOLE_1: 79;

      then

       A3: ( {} T) = ((A /\ B) /\ ((A /\ B) ` ));

      

       A4: ((A /\ B) /\ ( Int ((A /\ B) ` ))) c= ((A /\ B) /\ ((A /\ B) ` )) by TOPS_1: 16, XBOOLE_1: 26;

      then (A /\ (B /\ ( Int ((A /\ B) ` )))) = ( {} T) by A3, XBOOLE_1: 16;

      then A misses (B /\ ( Int ((A /\ B) ` )));

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

      then

       A5: ( Int (B /\ ( Int ((A /\ B) ` )))) c= ( Int (A ` )) by TOPS_1: 19;

      (B /\ (A /\ ( Int ((A /\ B) ` )))) = ( {} T) by A3, A4, XBOOLE_1: 16;

      then B misses (A /\ ( Int ((A /\ B) ` )));

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

      then

       A6: ( Int (A /\ ( Int ((A /\ B) ` )))) c= ( Int (B ` )) by TOPS_1: 19;

      assume

       A7: A is open or B is open;

       A8:

      now

        per cases by A7;

          suppose A is open;

          then (A /\ ( Int ((A /\ B) ` ))) c= ((( Int (B ` )) ` ) ` ) by A6, TOPS_1: 23;

          then (( Int (B ` )) ` ) misses (A /\ ( Int ((A /\ B) ` ))) by Th2;

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

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

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

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

          then (( Cl B) /\ ( Int ((A /\ B) ` ))) c= (A ` ) by Th2;

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

          then (( Int ( Cl B)) /\ ( Int ( Int ((A /\ B) ` )))) c= ( Int (A ` )) by TOPS_1: 17;

          then ((( Int ( Cl B)) /\ ( Int ((A /\ B) ` ))) /\ (( Int (A ` )) ` )) c= (( Int (A ` )) /\ (( Int (A ` )) ` )) by XBOOLE_1: 26;

          then ((( Int ( Cl B)) /\ ( Int ((A /\ B) ` ))) /\ (( Int (A ` )) ` )) c= ( {} T) by A1;

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

          then ( {} T) = (( Int ((A /\ B) ` )) /\ (( Int ( Cl B)) /\ ( Cl A))) by XBOOLE_1: 16;

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

          then (( Int ( Cl B)) /\ ( Cl A)) c= (( Int ((A /\ B) ` )) ` ) by Th2;

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

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

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

          hence (( Int ( Cl A)) /\ ( Int ( Cl B))) c= ( Int ( Cl (A /\ B)));

        end;

          suppose B is open;

          then (B /\ ( Int ((A /\ B) ` ))) c= ((( Int (A ` )) ` ) ` ) by A5, TOPS_1: 23;

          then (( Int (A ` )) ` ) misses (B /\ ( Int ((A /\ B) ` ))) by Th2;

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

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

          then (B /\ (( Cl A) /\ ( Int ((A /\ B) ` )))) = ( {} T) by XBOOLE_1: 16;

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

          then (( Cl A) /\ ( Int ((A /\ B) ` ))) c= (B ` ) by Th2;

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

          then (( Int ( Cl A)) /\ ( Int ( Int ((A /\ B) ` )))) c= ( Int (B ` )) by TOPS_1: 17;

          then ((( Int ( Cl A)) /\ ( Int ((A /\ B) ` ))) /\ (( Int (B ` )) ` )) c= (( Int (B ` )) /\ (( Int (B ` )) ` )) by XBOOLE_1: 26;

          then ((( Int ( Cl A)) /\ ( Int ((A /\ B) ` ))) /\ (( Int (B ` )) ` )) c= ( {} T) by A2;

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

          then ( {} T) = (( Int ((A /\ B) ` )) /\ (( Int ( Cl A)) /\ ( Cl B))) by XBOOLE_1: 16;

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

          then (( Int ( Cl A)) /\ ( Cl B)) c= (( Int ((A /\ B) ` )) ` ) by Th2;

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

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

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

          hence (( Int ( Cl A)) /\ ( Int ( Cl B))) c= ( Int ( Cl (A /\ B)));

        end;

      end;

      ( Cl (A /\ B)) c= ( Cl B) by PRE_TOPC: 19, XBOOLE_1: 17;

      then

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

      ( Cl (A /\ B)) c= ( Cl A) by PRE_TOPC: 19, XBOOLE_1: 17;

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

      then ( Int ( Cl (A /\ B))) c= (( Int ( Cl A)) /\ ( Int ( Cl B))) by A9, XBOOLE_1: 19;

      hence thesis by A8;

    end;

    theorem :: TDLAT_1:8

    

     Th8: for A be Subset of T holds ( Int (A /\ ( Cl (A ` )))) = ( {} T)

    proof

      let A be Subset of T;

      

       A1: ( Int A) misses (( Int A) ` ) by XBOOLE_1: 79;

      

      thus ( Int (A /\ ( Cl (A ` )))) = ( Int (A /\ ((( Cl (A ` )) ` ) ` )))

      .= ( Int (A /\ (( Int A) ` ))) by TOPS_1:def 1

      .= (( Int ( Int A)) /\ ( Int (( Int A) ` ))) by TOPS_1: 17

      .= ( Int (( Int A) /\ (( Int A) ` ))) by TOPS_1: 17

      .= ( Int ( {} T)) by A1

      .= ( {} T);

    end;

    theorem :: TDLAT_1:9

    

     Th9: for A be Subset of T holds ( Cl (A \/ ( Int (A ` )))) = ( [#] T)

    proof

      let A be Subset of T;

      

      thus ( Cl (A \/ ( Int (A ` )))) = ( Cl (A \/ (( Cl ((A ` ) ` )) ` ))) by TOPS_1:def 1

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

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

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

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

    end;

    theorem :: TDLAT_1:10

    

     Th10: for A,B be Subset of T holds (( Int ( Cl (A \/ (( Int ( Cl B)) \/ B)))) \/ (A \/ (( Int ( Cl B)) \/ B))) = (( Int ( Cl (A \/ B))) \/ (A \/ B))

    proof

      let A,B be Subset of T;

      ( Cl B) c= ( Cl (A \/ B)) by PRE_TOPC: 19, XBOOLE_1: 7;

      then

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

      (A \/ B) c= (A \/ (( Int ( Cl B)) \/ B)) by XBOOLE_1: 7, XBOOLE_1: 9;

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

      then

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

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

      then

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

      ( Int ( Cl (A \/ (( Int ( Cl B)) \/ B)))) = ( Int ( Cl ((A \/ ( Int ( Cl B))) \/ B))) by XBOOLE_1: 4

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

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

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

      .= ( Int (( Cl A) \/ ( Cl B))) by Th3, XBOOLE_1: 12

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

      then (( Int ( Cl (A \/ (( Int ( Cl B)) \/ B)))) \/ ( Int ( Cl B))) c= ( Int ( Cl (A \/ B))) by A1, XBOOLE_1: 8;

      then

       A4: (( Int ( Cl (A \/ (( Int ( Cl B)) \/ B)))) \/ ( Int ( Cl B))) = ( Int ( Cl (A \/ B))) by A3;

      (A \/ (( Int ( Cl B)) \/ B)) = (( Int ( Cl B)) \/ (A \/ B)) by XBOOLE_1: 4;

      hence thesis by A4, XBOOLE_1: 4;

    end;

    theorem :: TDLAT_1:11

    for A,C be Subset of T holds (( Int ( Cl ((( Int ( Cl A)) \/ A) \/ C))) \/ ((( Int ( Cl A)) \/ A) \/ C)) = (( Int ( Cl (A \/ C))) \/ (A \/ C)) by Th10;

    theorem :: TDLAT_1:12

    

     Th12: for A,B be Subset of T holds (( Cl ( Int (A /\ (( Cl ( Int B)) /\ B)))) /\ (A /\ (( Cl ( Int B)) /\ B))) = (( Cl ( Int (A /\ B))) /\ (A /\ B))

    proof

      let A,B be Subset of T;

      ( Int (A /\ B)) c= ( Int B) by TOPS_1: 19, XBOOLE_1: 17;

      then

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

      ( Cl ( Int (A /\ (( Cl ( Int B)) /\ B)))) = ( Cl ( Int ((A /\ ( Cl ( Int B))) /\ B))) by XBOOLE_1: 16

      .= ( Cl (( Int (A /\ ( Cl ( Int B)))) /\ ( Int B))) by TOPS_1: 17

      .= ( Cl ((( Int A) /\ ( Int ( Cl ( Int B)))) /\ ( Int B))) by TOPS_1: 17

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

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

      .= ( Cl ( Int (A /\ B))) by TOPS_1: 17;

      then

       A2: ( Cl ( Int (A /\ B))) c= (( Cl ( Int (A /\ (( Cl ( Int B)) /\ B)))) /\ ( Cl ( Int B))) by A1, XBOOLE_1: 19;

      (A /\ (( Cl ( Int B)) /\ B)) c= (A /\ B) by XBOOLE_1: 17, XBOOLE_1: 26;

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

      then

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

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

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

      then

       A4: (( Cl ( Int (A /\ (( Cl ( Int B)) /\ B)))) /\ ( Cl ( Int B))) = ( Cl ( Int (A /\ B))) by A2;

      (A /\ (( Cl ( Int B)) /\ B)) = (( Cl ( Int B)) /\ (A /\ B)) by XBOOLE_1: 16;

      hence thesis by A4, XBOOLE_1: 16;

    end;

    theorem :: TDLAT_1:13

    for A,C be Subset of T holds (( Cl ( Int ((( Cl ( Int A)) /\ A) /\ C))) /\ ((( Cl ( Int A)) /\ A) /\ C)) = (( Cl ( Int (A /\ C))) /\ (A /\ C)) by Th12;

    begin

    theorem :: TDLAT_1:14

    

     Th14: ( {} T) is condensed

    proof

      ( Int ( {} T)) c= ( {} T);

      then

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

      ( {} T) c= ( Cl ( Int ( {} T)));

      hence thesis by A1, TOPS_1:def 6;

    end;

    theorem :: TDLAT_1:15

    

     Th15: ( [#] T) is condensed

    proof

      ( [#] T) c= ( Cl ( [#] T)) by PRE_TOPC: 18;

      then

       A1: ( [#] T) c= ( Cl ( Int ( [#] T))) by TOPS_1: 15;

      ( Int ( Cl ( [#] T))) c= ( [#] T);

      hence thesis by A1, TOPS_1:def 6;

    end;

    theorem :: TDLAT_1:16

    

     Th16: for A be Subset of T st A is condensed holds (A ` ) is condensed

    proof

      let X be Subset of T;

      assume

       A1: X is condensed;

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

      then (( Cl ((( Int X) ` ) ` )) ` ) c= (X ` ) by SUBSET_1: 12;

      then ( Int (( Int X) ` )) c= (X ` ) by TOPS_1:def 1;

      then

       A2: ( Int ((( Cl (X ` )) ` ) ` )) c= (X ` ) by TOPS_1:def 1;

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

      then (( Cl (( Cl X) ` )) ` ) c= X by TOPS_1:def 1;

      then (X ` ) c= ( Cl (( Cl ((X ` ) ` )) ` )) by SUBSET_1: 12;

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

      hence thesis by A2, TOPS_1:def 6;

    end;

    theorem :: TDLAT_1:17

    

     Th17: for A,B be Subset of T st A is condensed & B is condensed holds (( Int ( Cl (A \/ B))) \/ (A \/ B)) is condensed & (( Cl ( Int (A /\ B))) /\ (A /\ B)) is condensed

    proof

      let A,B be Subset of T;

      assume

       A1: A is condensed;

      assume

       A2: B is condensed;

      then

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

      

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

      thus (( Int ( Cl (A \/ B))) \/ (A \/ B)) is condensed

      proof

        set X = (( Int ( Cl (A \/ B))) \/ (A \/ B));

        ( Cl (( Int A) \/ ( Int B))) c= ( Cl ( Int (A \/ B))) by PRE_TOPC: 19, TOPS_1: 20;

        then

         A5: (( Cl ( Int A)) \/ ( Cl ( Int B))) c= ( Cl ( Int (A \/ B))) by PRE_TOPC: 20;

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

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

        then

         A6: (( Int ( Cl (A \/ B))) \/ (A \/ B)) c= (( Int ( Cl (A \/ B))) \/ ( Cl ( Int (A \/ B)))) by XBOOLE_1: 9;

        ( Cl (( Int ( Int ( Cl (A \/ B)))) \/ ( Int (A \/ B)))) c= ( Cl ( Int X)) by PRE_TOPC: 19, TOPS_1: 20;

        then

         A7: (( Cl ( Int ( Cl (A \/ B)))) \/ ( Cl ( Int (A \/ B)))) c= ( Cl ( Int X)) by PRE_TOPC: 20;

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

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

        then ( Int ( Cl X)) = ( Int ( Cl (A \/ B))) by PRE_TOPC: 20;

        then

         A8: ( Int ( Cl X)) c= X by XBOOLE_1: 7;

        (( Int ( Cl (A \/ B))) \/ ( Cl ( Int (A \/ B)))) c= (( Cl ( Int ( Cl (A \/ B)))) \/ ( Cl ( Int (A \/ B)))) by PRE_TOPC: 18, XBOOLE_1: 9;

        then (( Int ( Cl (A \/ B))) \/ ( Cl ( Int (A \/ B)))) c= ( Cl ( Int X)) by A7;

        then X c= ( Cl ( Int X)) by A6;

        hence thesis by A8, TOPS_1:def 6;

      end;

      

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

      

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

      thus (( Cl ( Int (A /\ B))) /\ (A /\ B)) is condensed

      proof

        set X = (( Cl ( Int (A /\ B))) /\ (A /\ B));

        ( Int ( Cl (A /\ B))) c= ( Int (( Cl A) /\ ( Cl B))) by PRE_TOPC: 21, TOPS_1: 19;

        then

         A11: ( Int ( Cl (A /\ B))) c= (( Int ( Cl A)) /\ ( Int ( Cl B))) by TOPS_1: 17;

        (( Int ( Cl A)) /\ ( Int ( Cl B))) c= (A /\ B) by A10, A9, XBOOLE_1: 27;

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

        then

         A12: (( Cl ( Int (A /\ B))) /\ ( Int ( Cl (A /\ B)))) c= (( Cl ( Int (A /\ B))) /\ (A /\ B)) by XBOOLE_1: 26;

        ( Int ( Cl X)) c= ( Int (( Cl ( Cl ( Int (A /\ B)))) /\ ( Cl (A /\ B)))) by PRE_TOPC: 21, TOPS_1: 19;

        then

         A13: ( Int ( Cl X)) c= (( Int ( Cl ( Int (A /\ B)))) /\ ( Int ( Cl (A /\ B)))) by TOPS_1: 17;

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

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

        then ( Cl ( Int (A /\ B))) = ( Cl ( Int X)) by TOPS_1: 17;

        then

         A14: X c= ( Cl ( Int X)) by XBOOLE_1: 17;

        (( Int ( Cl ( Int (A /\ B)))) /\ ( Int ( Cl (A /\ B)))) c= (( Cl ( Int (A /\ B))) /\ ( Int ( Cl (A /\ B)))) by TOPS_1: 16, XBOOLE_1: 26;

        then ( Int ( Cl X)) c= (( Cl ( Int (A /\ B))) /\ ( Int ( Cl (A /\ B)))) by A13;

        then ( Int ( Cl X)) c= X by A12;

        hence thesis by A14, TOPS_1:def 6;

      end;

    end;

    theorem :: TDLAT_1:18

    

     Th18: ( {} T) is closed_condensed

    proof

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

      hence thesis by TOPS_1:def 7;

    end;

    theorem :: TDLAT_1:19

    

     Th19: ( [#] T) is closed_condensed

    proof

      ( Int ( [#] T)) = ( [#] T) by TOPS_1: 15;

      then ( Cl ( Int ( [#] T))) = ( [#] T) by TOPS_1: 2;

      hence thesis by TOPS_1:def 7;

    end;

    theorem :: TDLAT_1:20

    

     Th20: ( {} T) is open_condensed

    proof

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

      then ( Int ( Cl ( {} T))) = ( {} T);

      hence thesis by TOPS_1:def 8;

    end;

    theorem :: TDLAT_1:21

    

     Th21: ( [#] T) is open_condensed

    proof

      ( Cl ( [#] T)) = ( [#] T) by TOPS_1: 2;

      then ( Int ( Cl ( [#] T))) = ( [#] T) by TOPS_1: 15;

      hence thesis by TOPS_1:def 8;

    end;

    theorem :: TDLAT_1:22

    

     Th22: for A be Subset of T holds ( Cl ( Int A)) is closed_condensed

    proof

      let A be Subset of T;

      ( Cl ( Int A)) = ( Cl ( Int ( Cl ( Int A)))) by TOPS_1: 26;

      hence thesis by TOPS_1:def 7;

    end;

    theorem :: TDLAT_1:23

    

     Th23: for A be Subset of T holds ( Int ( Cl A)) is open_condensed

    proof

      let A be Subset of T;

      ( Int ( Cl A)) = ( Int ( Cl ( Int ( Cl A)))) by Th5;

      hence thesis by TOPS_1:def 8;

    end;

    theorem :: TDLAT_1:24

    

     Th24: for A be Subset of T st A is condensed holds ( Cl A) is closed_condensed

    proof

      let A be Subset of T;

      assume

       A1: A is condensed;

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

      then

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

      ( Cl A) is condensed by A1, TOPS_1: 71;

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

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

      hence thesis by TOPS_1:def 7;

    end;

    theorem :: TDLAT_1:25

    

     Th25: for A be Subset of T st A is condensed holds ( Int A) is open_condensed

    proof

      let A be Subset of T;

      assume

       A1: A is condensed;

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

      then

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

      ( Int A) is condensed by A1, TOPS_1: 71;

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

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

      hence thesis by TOPS_1:def 8;

    end;

    theorem :: TDLAT_1:26

    for A be Subset of T st A is condensed holds ( Cl (A ` )) is closed_condensed by Th16, Th24;

    theorem :: TDLAT_1:27

    for A be Subset of T st A is condensed holds ( Int (A ` )) is open_condensed by Th16, Th25;

    theorem :: TDLAT_1:28

    

     Th28: for A,B,C be Subset of T st A is closed_condensed & B is closed_condensed & C is closed_condensed holds ( Cl ( Int (A /\ ( Cl ( Int (B /\ C)))))) = ( Cl ( Int (( Cl ( Int (A /\ B))) /\ C)))

    proof

      let A,B,C be Subset of T;

      assume that

       A1: A is closed_condensed and

       A2: B is closed_condensed and

       A3: C is closed_condensed;

      

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

      

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

      

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

      

       A7: ( Cl ( Int (B /\ C))) = ( Cl (( Int B) /\ ( Int C))) by TOPS_1: 17;

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

      then (A /\ ( Cl ( Int (B /\ C)))) c= (A /\ (B /\ C)) by A7, A4, PRE_TOPC: 21, XBOOLE_1: 26;

      then

       A8: ( Int (A /\ ( Cl ( Int (B /\ C))))) c= (A /\ (B /\ C)) by A6;

      then ( Int (A /\ ( Cl ( Int (B /\ C))))) c= ((A /\ B) /\ C) by XBOOLE_1: 16;

      then

       A9: ( Int (A /\ ( Cl ( Int (B /\ C))))) c= C by A5;

      

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

      ( Int (A /\ ( Cl ( Int (B /\ C))))) c= ((A /\ B) /\ C) by A8, XBOOLE_1: 16;

      then ( Int (A /\ ( Cl ( Int (B /\ C))))) c= (A /\ B) by A10;

      then

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

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

      then ( Int (A /\ ( Cl ( Int (B /\ C))))) c= ( Cl ( Int (A /\ B))) by A11;

      then ( Int (A /\ ( Cl ( Int (B /\ C))))) c= (( Cl ( Int (A /\ B))) /\ C) by A9, XBOOLE_1: 19;

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

      then

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

      

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

      

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

      

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

      

       A16: ( Cl ( Int (A /\ B))) = ( Cl (( Int A) /\ ( Int B))) by TOPS_1: 17;

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

      then (( Cl ( Int (A /\ B))) /\ C) c= ((A /\ B) /\ C) by A16, A4, PRE_TOPC: 21, XBOOLE_1: 26;

      then

       A17: ( Int (( Cl ( Int (A /\ B))) /\ C)) c= ((A /\ B) /\ C) by A15;

      then ( Int (( Cl ( Int (A /\ B))) /\ C)) c= (A /\ (B /\ C)) by XBOOLE_1: 16;

      then

       A18: ( Int (( Cl ( Int (A /\ B))) /\ C)) c= A by A14;

      ( Int (( Cl ( Int (A /\ B))) /\ C)) c= (A /\ (B /\ C)) by A17, XBOOLE_1: 16;

      then ( Int (( Cl ( Int (A /\ B))) /\ C)) c= (B /\ C) by A13;

      then

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

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

      then ( Int (( Cl ( Int (A /\ B))) /\ C)) c= ( Cl ( Int (B /\ C))) by A19;

      then ( Int (( Cl ( Int (A /\ B))) /\ C)) c= (A /\ ( Cl ( Int (B /\ C)))) by A18, XBOOLE_1: 19;

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

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

      hence thesis by A12;

    end;

    theorem :: TDLAT_1:29

    

     Th29: for A,B,C be Subset of T st A is open_condensed & B is open_condensed & C is open_condensed holds ( Int ( Cl (A \/ ( Int ( Cl (B \/ C)))))) = ( Int ( Cl (( Int ( Cl (A \/ B))) \/ C)))

    proof

      let A,B,C be Subset of T;

      assume that

       A1: A is open_condensed and

       A2: B is open_condensed and

       A3: C is open_condensed;

      

       A4: B = ( Int ( Cl B)) by A2, TOPS_1:def 8;

      

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

      

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

      

       A7: ( Int ( Cl (B \/ C))) = ( Int (( Cl B) \/ ( Cl C))) by PRE_TOPC: 20;

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

      then (A \/ (B \/ C)) c= (A \/ ( Int ( Cl (B \/ C)))) by A7, A4, TOPS_1: 20, XBOOLE_1: 9;

      then

       A8: (A \/ (B \/ C)) c= ( Cl (A \/ ( Int ( Cl (B \/ C))))) by A6;

      then ((A \/ B) \/ C) c= ( Cl (A \/ ( Int ( Cl (B \/ C))))) by XBOOLE_1: 4;

      then

       A9: C c= ( Cl (A \/ ( Int ( Cl (B \/ C))))) by A5;

      

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

      ((A \/ B) \/ C) c= ( Cl (A \/ ( Int ( Cl (B \/ C))))) by A8, XBOOLE_1: 4;

      then (A \/ B) c= ( Cl (A \/ ( Int ( Cl (B \/ C))))) by A10;

      then

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

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

      then ( Int ( Cl (A \/ B))) c= ( Cl (A \/ ( Int ( Cl (B \/ C))))) by A11;

      then (( Int ( Cl (A \/ B))) \/ C) c= ( Cl (A \/ ( Int ( Cl (B \/ C))))) by A9, XBOOLE_1: 8;

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

      then

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

      

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

      

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

      

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

      

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

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

      then ((A \/ B) \/ C) c= (( Int ( Cl (A \/ B))) \/ C) by A16, A4, TOPS_1: 20, XBOOLE_1: 9;

      then

       A17: ((A \/ B) \/ C) c= ( Cl (( Int ( Cl (A \/ B))) \/ C)) by A15;

      then (A \/ (B \/ C)) c= ( Cl (( Int ( Cl (A \/ B))) \/ C)) by XBOOLE_1: 4;

      then

       A18: A c= ( Cl (( Int ( Cl (A \/ B))) \/ C)) by A14;

      (A \/ (B \/ C)) c= ( Cl (( Int ( Cl (A \/ B))) \/ C)) by A17, XBOOLE_1: 4;

      then (B \/ C) c= ( Cl (( Int ( Cl (A \/ B))) \/ C)) by A13;

      then

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

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

      then ( Int ( Cl (B \/ C))) c= ( Cl (( Int ( Cl (A \/ B))) \/ C)) by A19;

      then (A \/ ( Int ( Cl (B \/ C)))) c= ( Cl (( Int ( Cl (A \/ B))) \/ C)) by A18, XBOOLE_1: 8;

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

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

      hence thesis by A12;

    end;

    begin

    definition

      let T be TopStruct;

      :: TDLAT_1:def1

      func Domains_of T -> Subset-Family of T equals { A where A be Subset of T : A is condensed };

      coherence

      proof

        set B = { A where A be Subset of T : A is condensed };

        B c= ( bool the carrier of T)

        proof

          let x be object;

          assume x in B;

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

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let T be TopSpace;

      cluster ( Domains_of T) -> non empty;

      coherence

      proof

        ( {} T) is condensed by Th14;

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

        hence thesis;

      end;

    end

    definition

      let T be TopSpace;

      :: TDLAT_1:def2

      func Domains_Union T -> BinOp of ( Domains_of T) means

      : Def2: for A,B be Element of ( Domains_of T) holds (it . (A,B)) = (( Int ( Cl (A \/ B))) \/ (A \/ B));

      existence

      proof

        defpred X[ set, set] means for A,B be Element of ( Domains_of T) st $1 = [A, B] holds $2 = (( Int ( Cl (A \/ B))) \/ (A \/ B));

        set D = [:( Domains_of T), ( Domains_of T) qua non empty set:];

        

         A1: for a be Element of D holds ex b be Element of ( Domains_of T) st X[a, b]

        proof

          let a be Element of D;

          reconsider G = (a `1 ), F = (a `2 ) as Element of ( Domains_of T);

          F in { H where H be Subset of T : H is condensed };

          then

           A2: ex H be Subset of T st H = F & H is condensed;

          G in { E where E be Subset of T : E is condensed };

          then ex E be Subset of T st E = G & E is condensed;

          then (( Int ( Cl (G \/ F))) \/ (G \/ F)) is condensed by A2, Th17;

          then (( Int ( Cl (G \/ F))) \/ (G \/ F)) in { E where E be Subset of T : E is condensed };

          then

          reconsider b = (( Int ( Cl (G \/ F))) \/ (G \/ F)) as Element of ( Domains_of T);

          take b;

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

          assume a = [A, B];

          then

           A3: [A, B] = [G, F] by MCART_1: 21;

          then

           A4: B = F by XTUPLE_0: 1;

          A = G by A3, XTUPLE_0: 1;

          hence thesis by A4;

        end;

        consider h be Function of D, ( Domains_of T) such that

         A5: for a be Element of D holds X[a, (h . a)] from FUNCT_2:sch 3( A1);

        take h;

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

        

        thus (h . (A,B)) = (h . [A, B])

        .= (( Int ( Cl (A \/ B))) \/ (A \/ B)) by A5;

      end;

      uniqueness

      proof

        deffunc U( Element of ( Domains_of T), Element of ( Domains_of T)) = (( Int ( Cl ($1 \/ $2))) \/ ($1 \/ $2));

        thus for o1,o2 be BinOp of ( Domains_of T) st (for a,b be Element of ( Domains_of T) holds (o1 . (a,b)) = U(a,b)) & (for a,b be Element of ( Domains_of T) holds (o2 . (a,b)) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    notation

      let T be TopSpace;

      synonym D-Union T for Domains_Union T;

    end

    definition

      let T be TopSpace;

      :: TDLAT_1:def3

      func Domains_Meet T -> BinOp of ( Domains_of T) means

      : Def3: for A,B be Element of ( Domains_of T) holds (it . (A,B)) = (( Cl ( Int (A /\ B))) /\ (A /\ B));

      existence

      proof

        defpred X[ set, set] means for A,B be Element of ( Domains_of T) st $1 = [A, B] holds $2 = (( Cl ( Int (A /\ B))) /\ (A /\ B));

        set D = [:( Domains_of T), ( Domains_of T) qua non empty set:];

        

         A1: for a be Element of D holds ex b be Element of ( Domains_of T) st X[a, b]

        proof

          let a be Element of D;

          reconsider G = (a `1 ), F = (a `2 ) as Element of ( Domains_of T);

          F in { H where H be Subset of T : H is condensed };

          then

           A2: ex H be Subset of T st H = F & H is condensed;

          G in { E where E be Subset of T : E is condensed };

          then ex E be Subset of T st E = G & E is condensed;

          then (( Cl ( Int (G /\ F))) /\ (G /\ F)) is condensed by A2, Th17;

          then (( Cl ( Int (G /\ F))) /\ (G /\ F)) in { E where E be Subset of T : E is condensed };

          then

          reconsider b = (( Cl ( Int (G /\ F))) /\ (G /\ F)) as Element of ( Domains_of T);

          take b;

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

          assume a = [A, B];

          then

           A3: [A, B] = [G, F] by MCART_1: 21;

          then

           A4: B = F by XTUPLE_0: 1;

          A = G by A3, XTUPLE_0: 1;

          hence thesis by A4;

        end;

        consider h be Function of D, ( Domains_of T) such that

         A5: for a be Element of D holds X[a, (h . a)] from FUNCT_2:sch 3( A1);

        take h;

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

        

        thus (h . (A,B)) = (h . [A, B])

        .= (( Cl ( Int (A /\ B))) /\ (A /\ B)) by A5;

      end;

      uniqueness

      proof

        deffunc U( Element of ( Domains_of T), Element of ( Domains_of T)) = (( Cl ( Int ($1 /\ $2))) /\ ($1 /\ $2));

        thus for o1,o2 be BinOp of ( Domains_of T) st (for a,b be Element of ( Domains_of T) holds (o1 . (a,b)) = U(a,b)) & (for a,b be Element of ( Domains_of T) holds (o2 . (a,b)) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    notation

      let T be TopSpace;

      synonym D-Meet T for Domains_Meet T;

    end

    theorem :: TDLAT_1:30

    

     Th30: for T be TopSpace holds LattStr (# ( Domains_of T), ( D-Union T), ( D-Meet T) #) is C_Lattice

    proof

      let T be TopSpace;

      set L = LattStr (# ( Domains_of T), ( D-Union T), ( D-Meet T) #);

      

       A1: L is join-commutative

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Domains_of T);

        

        thus (a "\/" b) = (( Int ( Cl (B \/ A))) \/ (B \/ A)) by Def2

        .= (b "\/" a) by Def2;

      end;

      

       A2: L is meet-absorbing

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Domains_of T);

        

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

        B in { D where D be Subset of T : D is condensed };

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

        then

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

        

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

        (a "/\" b) = (( Cl ( Int (A /\ B))) /\ (A /\ B)) by Def3;

        

        hence ((a "/\" b) "\/" b) = (( Int ( Cl ((( Cl ( Int (A /\ B))) /\ (A /\ B)) \/ B))) \/ ((( Cl ( Int (A /\ B))) /\ (A /\ B)) \/ B)) by Def2

        .= (( Int ( Cl ((( Cl ( Int (A /\ B))) /\ (A /\ B)) \/ B))) \/ B) by A3, A5, XBOOLE_1: 1, XBOOLE_1: 12

        .= (( Int ( Cl B)) \/ B) by A3, A5, XBOOLE_1: 1, XBOOLE_1: 12

        .= b by A4, XBOOLE_1: 12;

      end;

      

       A6: L is join-associative

      proof

        let a,b,c be Element of L;

        reconsider A = a, B = b, C = c as Element of ( Domains_of T);

        

         A7: (a "\/" b) = (( Int ( Cl (A \/ B))) \/ (A \/ B)) by Def2;

        (b "\/" c) = (( Int ( Cl (B \/ C))) \/ (B \/ C)) by Def2;

        

        hence (a "\/" (b "\/" c)) = (( Int ( Cl (A \/ (( Int ( Cl (B \/ C))) \/ (B \/ C))))) \/ (A \/ (( Int ( Cl (B \/ C))) \/ (B \/ C)))) by Def2

        .= (( Int ( Cl (A \/ (B \/ C)))) \/ (A \/ (B \/ C))) by Th10

        .= (( Int ( Cl (A \/ (B \/ C)))) \/ ((A \/ B) \/ C)) by XBOOLE_1: 4

        .= (( Int ( Cl ((A \/ B) \/ C))) \/ ((A \/ B) \/ C)) by XBOOLE_1: 4

        .= (( Int ( Cl ((( Int ( Cl (A \/ B))) \/ (A \/ B)) \/ C))) \/ ((( Int ( Cl (A \/ B))) \/ (A \/ B)) \/ C)) by Th10

        .= ((a "\/" b) "\/" c) by A7, Def2;

      end;

      

       A8: L is meet-commutative

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Domains_of T);

        

        thus (a "/\" b) = (( Cl ( Int (B /\ A))) /\ (B /\ A)) by Def3

        .= (b "/\" a) by Def3;

      end;

      

       A9: L is join-absorbing

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Domains_of T);

        

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

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

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

        then

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

        

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

        (a "\/" b) = (( Int ( Cl (A \/ B))) \/ (A \/ B)) by Def2;

        

        hence (a "/\" (a "\/" b)) = (( Cl ( Int (A /\ (( Int ( Cl (A \/ B))) \/ (A \/ B))))) /\ (A /\ (( Int ( Cl (A \/ B))) \/ (A \/ B)))) by Def3

        .= (( Cl ( Int (A /\ (( Int ( Cl (A \/ B))) \/ (A \/ B))))) /\ A) by A10, A12, XBOOLE_1: 1, XBOOLE_1: 28

        .= (( Cl ( Int A)) /\ A) by A10, A12, XBOOLE_1: 1, XBOOLE_1: 28

        .= a by A11, XBOOLE_1: 28;

      end;

      L is meet-associative

      proof

        let a,b,c be Element of L;

        reconsider A = a, B = b, C = c as Element of ( Domains_of T);

        

         A13: (a "/\" b) = (( Cl ( Int (A /\ B))) /\ (A /\ B)) by Def3;

        (b "/\" c) = (( Cl ( Int (B /\ C))) /\ (B /\ C)) by Def3;

        

        hence (a "/\" (b "/\" c)) = (( Cl ( Int (A /\ (( Cl ( Int (B /\ C))) /\ (B /\ C))))) /\ (A /\ (( Cl ( Int (B /\ C))) /\ (B /\ C)))) by Def3

        .= (( Cl ( Int (A /\ (B /\ C)))) /\ (A /\ (B /\ C))) by Th12

        .= (( Cl ( Int (A /\ (B /\ C)))) /\ ((A /\ B) /\ C)) by XBOOLE_1: 16

        .= (( Cl ( Int ((A /\ B) /\ C))) /\ ((A /\ B) /\ C)) by XBOOLE_1: 16

        .= (( Cl ( Int ((( Cl ( Int (A /\ B))) /\ (A /\ B)) /\ C))) /\ ((( Cl ( Int (A /\ B))) /\ (A /\ B)) /\ C)) by Th12

        .= ((a "/\" b) "/\" c) by A13, Def3;

      end;

      then

      reconsider L as Lattice by A1, A6, A2, A8, A9;

      

       A14: L is lower-bounded

      proof

        ( {} T) is condensed by Th14;

        then ( {} T) in { D where D be Subset of T : D is condensed };

        then

        reconsider c = ( {} T) as Element of L;

        take c;

        let a be Element of L;

        reconsider C = c, A = a as Element of ( Domains_of T);

        (C /\ A) = C;

        

        hence (c "/\" a) = (( Cl ( Int C)) /\ C) by Def3

        .= c;

        hence (a "/\" c) = c;

      end;

      L is upper-bounded

      proof

        ( [#] T) is condensed by Th15;

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

        then

        reconsider c = ( [#] T) as Element of L;

        take c;

        let a be Element of L;

        reconsider C = c, A = a as Element of ( Domains_of T);

        (C \/ A) = C by XBOOLE_1: 12;

        

        hence (c "\/" a) = (( Int ( Cl C)) \/ C) by Def2

        .= c by XBOOLE_1: 12;

        hence (a "\/" c) = c;

      end;

      then

      reconsider L as 01_Lattice by A14;

      L is complemented

      proof

        ( [#] T) is condensed by Th15;

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

        then

        reconsider c = ( [#] T) as Element of L;

        let b be Element of L;

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

        

         A15: (B ` ) misses B by XBOOLE_1: 79;

        B in { D where D be Subset of T : D is condensed };

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

        then (B ` ) is condensed by Th16;

        then (B ` ) in { D where D be Subset of T : D is condensed };

        then

        reconsider a = (B ` ) as Element of L;

        take a;

        

         A16: for v be Element of L holds (the L_meet of L . (c,v)) = v

        proof

          let v be Element of L;

          reconsider V = v as Element of ( Domains_of T);

          V in { D where D be Subset of T : D is condensed };

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

          then

           A17: V c= ( Cl ( Int V)) by TOPS_1:def 6;

          

          thus (the L_meet of L . (c,v)) = (( Cl ( Int (( [#] T) /\ V))) /\ (( [#] T) /\ V)) by Def3

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

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

          .= v by A17, XBOOLE_1: 28;

        end;

        

        thus (a "\/" b) = (( Int ( Cl ((B ` ) \/ B))) \/ ((B ` ) \/ B)) by Def2

        .= (( Int ( Cl ((B ` ) \/ B))) \/ ( [#] T)) by PRE_TOPC: 2

        .= c by XBOOLE_1: 12

        .= ( Top L) by A16, LATTICE2: 17;

        hence (b "\/" a) = ( Top L);

        ( {} T) is condensed by Th14;

        then ( {} T) in { D where D be Subset of T : D is condensed };

        then

        reconsider c = ( {} T) as Element of L;

        

         A18: for v be Element of L holds (the L_join of L . (c,v)) = v

        proof

          let v be Element of L;

          reconsider V = v as Element of ( Domains_of T);

          V in { D where D be Subset of T : D is condensed };

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

          then

           A19: ( Int ( Cl V)) c= V by TOPS_1:def 6;

          

          thus (the L_join of L . (c,v)) = (( Int ( Cl (( {} T) \/ V))) \/ (( {} T) \/ V)) by Def2

          .= (( Int ( Cl ((( [#] T) ` ) \/ V))) \/ (( {} T) \/ V)) by XBOOLE_1: 37

          .= (( Int ( Cl ((( [#] T) ` ) \/ ((V ` ) ` )))) \/ ((( [#] T) ` ) \/ V)) by XBOOLE_1: 37

          .= (( Int ( Cl ((( [#] T) /\ (V ` )) ` ))) \/ ((( [#] T) ` ) \/ ((V ` ) ` ))) by XBOOLE_1: 54

          .= (( Int ( Cl ((( [#] T) /\ (V ` )) ` ))) \/ ((( [#] T) /\ (V ` )) ` )) by XBOOLE_1: 54

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

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

          .= v by A19, XBOOLE_1: 12;

        end;

        

        thus (a "/\" b) = (( Cl ( Int ((B ` ) /\ B))) /\ ((B ` ) /\ B)) by Def3

        .= (( Cl ( Int ((B ` ) /\ B))) /\ ( {} T)) by A15

        .= ( Bottom L) by A18, LATTICE2: 15;

        hence (b "/\" a) = ( Bottom L);

      end;

      hence thesis;

    end;

    definition

      let T be TopSpace;

      :: TDLAT_1:def4

      func Domains_Lattice T -> C_Lattice equals LattStr (# ( Domains_of T), ( Domains_Union T), ( Domains_Meet T) #);

      coherence by Th30;

    end

    begin

    definition

      let T be TopStruct;

      :: TDLAT_1:def5

      func Closed_Domains_of T -> Subset-Family of T equals { A where A be Subset of T : A is closed_condensed };

      coherence

      proof

        set B = { A where A be Subset of T : A is closed_condensed };

        B c= ( bool the carrier of T)

        proof

          let x be object;

          assume x in B;

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

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let T be TopSpace;

      cluster ( Closed_Domains_of T) -> non empty;

      coherence

      proof

        ( {} T) is closed_condensed by Th18;

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

        hence thesis;

      end;

    end

    theorem :: TDLAT_1:31

    

     Th31: for T be TopSpace holds ( Closed_Domains_of T) c= ( Domains_of T)

    proof

      let T be TopSpace;

      let x be object;

      assume x in ( Closed_Domains_of T);

      then x in { A where A be Subset of T : A is closed_condensed };

      then

      consider A1 be Subset of T such that

       A1: x = A1 & A1 is closed_condensed;

      A1 is condensed by A1, TOPS_1: 66;

      then x in { A where A be Subset of T : A is condensed } by A1;

      hence thesis;

    end;

    definition

      let T be TopSpace;

      :: TDLAT_1:def6

      func Closed_Domains_Union T -> BinOp of ( Closed_Domains_of T) means

      : Def6: for A,B be Element of ( Closed_Domains_of T) holds (it . (A,B)) = (A \/ B);

      existence

      proof

        defpred X[ set, set] means for A,B be Element of ( Closed_Domains_of T) st $1 = [A, B] holds $2 = (A \/ B);

        set D = [:( Closed_Domains_of T), ( Closed_Domains_of T) qua non empty set:];

        

         A1: for a be Element of D holds ex b be Element of ( Closed_Domains_of T) st X[a, b]

        proof

          let a be Element of D;

          reconsider G = (a `1 ), F = (a `2 ) as Element of ( Closed_Domains_of T);

          G in { E where E be Subset of T : E is closed_condensed };

          then

          consider E be Subset of T such that

           A2: E = G and

           A3: E is closed_condensed;

          F in { H where H be Subset of T : H is closed_condensed };

          then

          consider H be Subset of T such that

           A4: H = F and

           A5: H is closed_condensed;

          (E \/ H) is closed_condensed by A3, A5, TOPS_1: 68;

          then (G \/ F) in { K where K be Subset of T : K is closed_condensed } by A2, A4;

          then

          reconsider b = (G \/ F) as Element of ( Closed_Domains_of T);

          take b;

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

          assume a = [A, B];

          then

           A6: [A, B] = [G, F] by MCART_1: 21;

          then A = G by XTUPLE_0: 1;

          hence thesis by A6, XTUPLE_0: 1;

        end;

        consider h be Function of D, ( Closed_Domains_of T) such that

         A7: for a be Element of D holds X[a, (h . a)] from FUNCT_2:sch 3( A1);

        take h;

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

        

        thus (h . (A,B)) = (h . [A, B])

        .= (A \/ B) by A7;

      end;

      uniqueness

      proof

        deffunc U( Element of ( Closed_Domains_of T), Element of ( Closed_Domains_of T)) = ($1 \/ $2);

        thus for o1,o2 be BinOp of ( Closed_Domains_of T) st (for a,b be Element of ( Closed_Domains_of T) holds (o1 . (a,b)) = U(a,b)) & (for a,b be Element of ( Closed_Domains_of T) holds (o2 . (a,b)) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    notation

      let T be TopSpace;

      synonym CLD-Union T for Closed_Domains_Union T;

    end

    theorem :: TDLAT_1:32

    

     Th32: for A,B be Element of ( Closed_Domains_of T) holds (( CLD-Union T) . (A,B)) = (( D-Union T) . (A,B))

    proof

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

      

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

      ( Closed_Domains_of T) c= ( Domains_of T) by Th31;

      then

      reconsider A0 = A, B0 = B as Element of ( Domains_of T);

      B in { E where E be Subset of T : E is closed_condensed };

      then

      consider E be Subset of T such that

       A2: E = B and

       A3: E is closed_condensed;

      consider D be Subset of T such that

       A4: D = A and

       A5: D is closed_condensed by A1;

      (D \/ E) is closed_condensed by A5, A3, TOPS_1: 68;

      then (D \/ E) is condensed by TOPS_1: 66;

      then

       A6: ( Int ( Cl (A \/ B))) c= (A \/ B) by A4, A2, TOPS_1:def 6;

      

      thus (( CLD-Union T) . (A,B)) = (A \/ B) by Def6

      .= (( Int ( Cl (A0 \/ B0))) \/ (A0 \/ B0)) by A6, XBOOLE_1: 12

      .= (( D-Union T) . (A,B)) by Def2;

    end;

    definition

      let T be TopSpace;

      :: TDLAT_1:def7

      func Closed_Domains_Meet T -> BinOp of ( Closed_Domains_of T) means

      : Def7: for A,B be Element of ( Closed_Domains_of T) holds (it . (A,B)) = ( Cl ( Int (A /\ B)));

      existence

      proof

        defpred X[ set, set] means for A,B be Element of ( Closed_Domains_of T) st $1 = [A, B] holds $2 = ( Cl ( Int (A /\ B)));

        set D = [:( Closed_Domains_of T), ( Closed_Domains_of T):];

        

         A1: for a be Element of D holds ex b be Element of ( Closed_Domains_of T) st X[a, b]

        proof

          let a be Element of D;

          reconsider G = (a `1 ), F = (a `2 ) as Element of ( Closed_Domains_of T);

          ( Cl ( Int (G /\ F))) is closed_condensed by Th22;

          then ( Cl ( Int (G /\ F))) in { E where E be Subset of T : E is closed_condensed };

          then

          reconsider b = ( Cl ( Int (G /\ F))) as Element of ( Closed_Domains_of T);

          take b;

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

          assume a = [A, B];

          then

           A2: [A, B] = [G, F] by MCART_1: 21;

          then A = G by XTUPLE_0: 1;

          hence thesis by A2, XTUPLE_0: 1;

        end;

        consider h be Function of D, ( Closed_Domains_of T) such that

         A3: for a be Element of D holds X[a, (h . a)] from FUNCT_2:sch 3( A1);

        take h;

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

        

        thus (h . (A,B)) = (h . [A, B])

        .= ( Cl ( Int (A /\ B))) by A3;

      end;

      uniqueness

      proof

        deffunc U( Element of ( Closed_Domains_of T), Element of ( Closed_Domains_of T)) = ( Cl ( Int ($1 /\ $2)));

        thus for o1,o2 be BinOp of ( Closed_Domains_of T) st (for a,b be Element of ( Closed_Domains_of T) holds (o1 . (a,b)) = U(a,b)) & (for a,b be Element of ( Closed_Domains_of T) holds (o2 . (a,b)) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    notation

      let T be TopSpace;

      synonym CLD-Meet T for Closed_Domains_Meet T;

    end

    theorem :: TDLAT_1:33

    

     Th33: for A,B be Element of ( Closed_Domains_of T) holds (( CLD-Meet T) . (A,B)) = (( D-Meet T) . (A,B))

    proof

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

      A in { D where D be Subset of T : D is closed_condensed };

      then

      consider D be Subset of T such that

       A1: D = A and

       A2: D is closed_condensed;

      

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

      ( Closed_Domains_of T) c= ( Domains_of T) by Th31;

      then

      reconsider A0 = A, B0 = B as Element of ( Domains_of T);

      B in { E where E be Subset of T : E is closed_condensed };

      then

      consider E be Subset of T such that

       A4: E = B and

       A5: E is closed_condensed;

      

       A6: E is closed by A5, TOPS_1: 66;

      D is closed by A2, TOPS_1: 66;

      then

       A7: ( Cl (D /\ E)) = (D /\ E) by A6, PRE_TOPC: 22;

      

      thus (( CLD-Meet T) . (A,B)) = ( Cl ( Int (A /\ B))) by Def7

      .= (( Cl ( Int (A0 /\ B0))) /\ (A0 /\ B0)) by A1, A4, A7, A3, PRE_TOPC: 19, XBOOLE_1: 28

      .= (( D-Meet T) . (A,B)) by Def3;

    end;

    theorem :: TDLAT_1:34

    

     Th34: for T be TopSpace holds LattStr (# ( Closed_Domains_of T), ( CLD-Union T), ( CLD-Meet T) #) is B_Lattice

    proof

      let T be TopSpace;

      set L = LattStr (# ( Closed_Domains_of T), ( CLD-Union T), ( CLD-Meet T) #);

      

       A1: L is join-commutative

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Closed_Domains_of T);

        

        thus (a "\/" b) = (B \/ A) by Def6

        .= (b "\/" a) by Def6;

      end;

      

       A2: L is meet-absorbing

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Closed_Domains_of T);

        

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

        B in { D where D be Subset of T : D is closed_condensed };

        then ex D be Subset of T st D = B & D is closed_condensed;

        then

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

        ( Cl ( Int (A /\ B))) = ( Cl (( Int A) /\ ( Int B))) by TOPS_1: 17;

        then

         A5: ( Cl ( Int (A /\ B))) c= (( Cl ( Int A)) /\ B) by A4, PRE_TOPC: 21;

        (a "/\" b) = ( Cl ( Int (A /\ B))) by Def7;

        

        hence ((a "/\" b) "\/" b) = (( Cl ( Int (A /\ B))) \/ B) by Def6

        .= b by A5, A3, XBOOLE_1: 1, XBOOLE_1: 12;

      end;

      

       A6: L is join-absorbing

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Closed_Domains_of T);

        A in { D where D be Subset of T : D is closed_condensed };

        then

         A7: ex D be Subset of T st D = A & D is closed_condensed;

        (a "\/" b) = (A \/ B) by Def6;

        

        hence (a "/\" (a "\/" b)) = ( Cl ( Int (A /\ (A \/ B)))) by Def7

        .= ( Cl ( Int A)) by XBOOLE_1: 21

        .= a by A7, TOPS_1:def 7;

      end;

      

       A8: L is join-associative

      proof

        let a,b,c be Element of L;

        reconsider A = a, B = b, C = c as Element of ( Closed_Domains_of T);

        

         A9: (a "\/" b) = (A \/ B) by Def6;

        (b "\/" c) = (B \/ C) by Def6;

        

        hence (a "\/" (b "\/" c)) = (A \/ (B \/ C)) by Def6

        .= ((A \/ B) \/ C) by XBOOLE_1: 4

        .= ((a "\/" b) "\/" c) by A9, Def6;

      end;

      

       A10: L is meet-associative

      proof

        let a,b,c be Element of L;

        reconsider A = a, B = b, C = c as Element of ( Closed_Domains_of T);

        A in { D where D be Subset of T : D is closed_condensed };

        then

         A11: ex D be Subset of T st D = A & D is closed_condensed;

        B in { E where E be Subset of T : E is closed_condensed };

        then

         A12: ex E be Subset of T st E = B & E is closed_condensed;

        C in { F where F be Subset of T : F is closed_condensed };

        then

         A13: ex F be Subset of T st F = C & F is closed_condensed;

        

         A14: (a "/\" b) = ( Cl ( Int (A /\ B))) by Def7;

        (b "/\" c) = ( Cl ( Int (B /\ C))) by Def7;

        

        hence (a "/\" (b "/\" c)) = ( Cl ( Int (A /\ ( Cl ( Int (B /\ C)))))) by Def7

        .= ( Cl ( Int (( Cl ( Int (A /\ B))) /\ C))) by A11, A12, A13, Th28

        .= ((a "/\" b) "/\" c) by A14, Def7;

      end;

      L is meet-commutative

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Closed_Domains_of T);

        

        thus (a "/\" b) = ( Cl ( Int (B /\ A))) by Def7

        .= (b "/\" a) by Def7;

      end;

      then

      reconsider L as Lattice by A1, A8, A2, A10, A6;

      

       A15: L is upper-bounded

      proof

        ( [#] T) is closed_condensed by Th19;

        then ( [#] T) in { D where D be Subset of T : D is closed_condensed };

        then

        reconsider c = ( [#] T) as Element of L;

        take c;

        let a be Element of L;

        reconsider C = c, A = a as Element of ( Closed_Domains_of T);

        

        thus (c "\/" a) = (C \/ A) by Def6

        .= c by XBOOLE_1: 12;

        hence (a "\/" c) = c;

      end;

      

       A16: L is distributive

      proof

        let a,b,c be Element of L;

        reconsider A = a, B = b, C = c as Element of ( Closed_Domains_of T);

        A in { D where D be Subset of T : D is closed_condensed };

        then

        consider D be Subset of T such that

         A17: D = A and

         A18: D is closed_condensed;

        

         A19: D is closed by A18, TOPS_1: 66;

        B in { E where E be Subset of T : E is closed_condensed };

        then

        consider E be Subset of T such that

         A20: E = B and

         A21: E is closed_condensed;

        

         A22: E is closed by A21, TOPS_1: 66;

        

         A23: (a "/\" c) = ( Cl ( Int (A /\ C))) by Def7;

        

         A24: (a "/\" b) = ( Cl ( Int (A /\ B))) by Def7;

        (b "\/" c) = (B \/ C) by Def6;

        

        hence (a "/\" (b "\/" c)) = ( Cl ( Int (A /\ (B \/ C)))) by Def7

        .= ( Cl ( Int ((A /\ B) \/ (A /\ C)))) by XBOOLE_1: 23

        .= (( Cl ( Int (A /\ B))) \/ ( Cl ( Int (A /\ C)))) by A17, A20, A19, A22, Th6

        .= ((a "/\" b) "\/" (a "/\" c)) by A24, A23, Def6;

      end;

      

       A25: L is complemented

      proof

        ( [#] T) is closed_condensed by Th19;

        then ( [#] T) in { K where K be Subset of T : K is closed_condensed };

        then

        reconsider c = ( [#] T) as Element of L;

        let b be Element of L;

        reconsider B = b as Element of ( Closed_Domains_of T);

        B in { D where D be Subset of T : D is closed_condensed };

        then

        consider D be Subset of T such that

         A26: D = B and

         A27: D is closed_condensed;

        D is condensed by A27, TOPS_1: 66;

        then ( Cl (B ` )) is closed_condensed by A26, Th16, Th24;

        then ( Cl (B ` )) in { K where K be Subset of T : K is closed_condensed };

        then

        reconsider a = ( Cl (B ` )) as Element of L;

        take a;

        

         A28: D is closed by A27, TOPS_1: 66;

        

         A29: for v be Element of L holds (the L_meet of L . (c,v)) = v

        proof

          let v be Element of L;

          reconsider V = v as Element of ( Closed_Domains_of T);

          V in { K where K be Subset of T : K is closed_condensed };

          then

           A30: ex D be Subset of T st D = V & D is closed_condensed;

          

          thus (the L_meet of L . (c,v)) = ( Cl ( Int (( [#] T) /\ V))) by Def7

          .= ( Cl ( Int V)) by XBOOLE_1: 28

          .= v by A30, TOPS_1:def 7;

        end;

        

        thus (a "\/" b) = (( Cl (B ` )) \/ B) by Def6

        .= (( Cl (D ` )) \/ ( Cl D)) by A26, A28, PRE_TOPC: 22

        .= ( Cl ((B ` ) \/ B)) by A26, PRE_TOPC: 20

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

        .= c by TOPS_1: 2

        .= ( Top L) by A29, LATTICE2: 17;

        hence (b "\/" a) = ( Top L);

        ( {} T) is closed_condensed by Th18;

        then ( {} T) in { K where K be Subset of T : K is closed_condensed };

        then

        reconsider c = ( {} T) as Element of L;

        

         A31: for v be Element of L holds (the L_join of L . (c,v)) = v

        proof

          let v be Element of L;

          reconsider V = v as Element of ( Closed_Domains_of T);

          

          thus (the L_join of L . (c,v)) = (( {} T) \/ V) by Def6

          .= ((( [#] T) ` ) \/ ((V ` ) ` )) by XBOOLE_1: 37

          .= ((( [#] T) /\ (V ` )) ` ) by XBOOLE_1: 54

          .= ((V ` ) ` ) by XBOOLE_1: 28

          .= v;

        end;

        

        thus (a "/\" b) = ( Cl ( Int (B /\ ( Cl (B ` ))))) by Def7

        .= ( Cl ( {} T)) by Th8

        .= c by PRE_TOPC: 22

        .= ( Bottom L) by A31, LATTICE2: 15;

        hence (b "/\" a) = ( Bottom L);

      end;

      L is lower-bounded

      proof

        

         A32: ( {} T) is closed_condensed by Th18;

        then ( {} T) in { D where D be Subset of T : D is closed_condensed };

        then

        reconsider c = ( {} T) as Element of L;

        take c;

        let a be Element of L;

        reconsider C = c, A = a as Element of ( Closed_Domains_of T);

        

        thus (c "/\" a) = ( Cl ( Int (C /\ A))) by Def7

        .= c by A32, TOPS_1:def 7;

        hence (a "/\" c) = c;

      end;

      hence thesis by A15, A25, A16;

    end;

    definition

      let T be TopSpace;

      :: TDLAT_1:def8

      func Closed_Domains_Lattice T -> B_Lattice equals LattStr (# ( Closed_Domains_of T), ( Closed_Domains_Union T), ( Closed_Domains_Meet T) #);

      coherence by Th34;

    end

    begin

    definition

      let T be TopStruct;

      :: TDLAT_1:def9

      func Open_Domains_of T -> Subset-Family of T equals { A where A be Subset of T : A is open_condensed };

      coherence

      proof

        set B = { A where A be Subset of T : A is open_condensed };

        B c= ( bool the carrier of T)

        proof

          let x be object;

          assume x in B;

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

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let T be TopSpace;

      cluster ( Open_Domains_of T) -> non empty;

      coherence

      proof

        ( {} T) is open_condensed by Th20;

        then ( {} T) in { A where A be Subset of T : A is open_condensed };

        hence thesis;

      end;

    end

    theorem :: TDLAT_1:35

    

     Th35: for T be TopSpace holds ( Open_Domains_of T) c= ( Domains_of T)

    proof

      let T be TopSpace;

      let x be object;

      assume x in ( Open_Domains_of T);

      then x in { A where A be Subset of T : A is open_condensed };

      then

      consider A1 be Subset of T such that

       A1: x = A1 & A1 is open_condensed;

      A1 is condensed by A1, TOPS_1: 67;

      then x in { A where A be Subset of T : A is condensed } by A1;

      hence thesis;

    end;

    definition

      let T be TopSpace;

      :: TDLAT_1:def10

      func Open_Domains_Union T -> BinOp of ( Open_Domains_of T) means

      : Def10: for A,B be Element of ( Open_Domains_of T) holds (it . (A,B)) = ( Int ( Cl (A \/ B)));

      existence

      proof

        defpred X[ set, set] means for A,B be Element of ( Open_Domains_of T) st $1 = [A, B] holds $2 = ( Int ( Cl (A \/ B)));

        set D = [:( Open_Domains_of T), ( Open_Domains_of T) qua non empty set:];

        

         A1: for a be Element of D holds ex b be Element of ( Open_Domains_of T) st X[a, b]

        proof

          let a be Element of D;

          reconsider G = (a `1 ), F = (a `2 ) as Element of ( Open_Domains_of T);

          ( Int ( Cl (G \/ F))) is open_condensed by Th23;

          then ( Int ( Cl (G \/ F))) in { E where E be Subset of T : E is open_condensed };

          then

          reconsider b = ( Int ( Cl (G \/ F))) as Element of ( Open_Domains_of T);

          take b;

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

          assume a = [A, B];

          then

           A2: [A, B] = [G, F] by MCART_1: 21;

          then A = G by XTUPLE_0: 1;

          hence thesis by A2, XTUPLE_0: 1;

        end;

        consider h be Function of D, ( Open_Domains_of T) such that

         A3: for a be Element of D holds X[a, (h . a)] from FUNCT_2:sch 3( A1);

        take h;

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

        

        thus (h . (A,B)) = (h . [A, B])

        .= ( Int ( Cl (A \/ B))) by A3;

      end;

      uniqueness

      proof

        deffunc U( Element of ( Open_Domains_of T), Element of ( Open_Domains_of T)) = ( Int ( Cl ($1 \/ $2)));

        thus for o1,o2 be BinOp of ( Open_Domains_of T) st (for a,b be Element of ( Open_Domains_of T) holds (o1 . (a,b)) = U(a,b)) & (for a,b be Element of ( Open_Domains_of T) holds (o2 . (a,b)) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    notation

      let T be TopSpace;

      synonym OPD-Union T for Open_Domains_Union T;

    end

    theorem :: TDLAT_1:36

    

     Th36: for A,B be Element of ( Open_Domains_of T) holds (( OPD-Union T) . (A,B)) = (( D-Union T) . (A,B))

    proof

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

      A in { D where D be Subset of T : D is open_condensed };

      then

      consider D be Subset of T such that

       A1: D = A and

       A2: D is open_condensed;

      

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

      ( Open_Domains_of T) c= ( Domains_of T) by Th35;

      then

      reconsider A0 = A, B0 = B as Element of ( Domains_of T);

      B in { E where E be Subset of T : E is open_condensed };

      then

      consider E be Subset of T such that

       A4: E = B and

       A5: E is open_condensed;

      

       A6: E is open by A5, TOPS_1: 67;

      D is open by A2, TOPS_1: 67;

      then

       A7: ( Int (D \/ E)) = (D \/ E) by A6, TOPS_1: 23;

      

      thus (( OPD-Union T) . (A,B)) = ( Int ( Cl (A \/ B))) by Def10

      .= (( Int ( Cl (A0 \/ B0))) \/ (A0 \/ B0)) by A1, A4, A7, A3, TOPS_1: 19, XBOOLE_1: 12

      .= (( D-Union T) . (A,B)) by Def2;

    end;

    definition

      let T be TopSpace;

      :: TDLAT_1:def11

      func Open_Domains_Meet T -> BinOp of ( Open_Domains_of T) means

      : Def11: for A,B be Element of ( Open_Domains_of T) holds (it . (A,B)) = (A /\ B);

      existence

      proof

        defpred X[ set, set] means for A,B be Element of ( Open_Domains_of T) st $1 = [A, B] holds $2 = (A /\ B);

        set D = [:( Open_Domains_of T), ( Open_Domains_of T) qua non empty set:];

        

         A1: for a be Element of D holds ex b be Element of ( Open_Domains_of T) st X[a, b]

        proof

          let a be Element of D;

          reconsider G = (a `1 ), F = (a `2 ) as Element of ( Open_Domains_of T);

          G in { E where E be Subset of T : E is open_condensed };

          then

          consider E be Subset of T such that

           A2: E = G and

           A3: E is open_condensed;

          F in { H where H be Subset of T : H is open_condensed };

          then

          consider H be Subset of T such that

           A4: H = F and

           A5: H is open_condensed;

          (E /\ H) is open_condensed by A3, A5, TOPS_1: 69;

          then (G /\ F) in { K where K be Subset of T : K is open_condensed } by A2, A4;

          then

          reconsider b = (G /\ F) as Element of ( Open_Domains_of T);

          take b;

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

          assume a = [A, B];

          then

           A6: [A, B] = [G, F] by MCART_1: 21;

          then A = G by XTUPLE_0: 1;

          hence thesis by A6, XTUPLE_0: 1;

        end;

        consider h be Function of D, ( Open_Domains_of T) such that

         A7: for a be Element of D holds X[a, (h . a)] from FUNCT_2:sch 3( A1);

        take h;

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

        

        thus (h . (A,B)) = (h . [A, B])

        .= (A /\ B) by A7;

      end;

      uniqueness

      proof

        deffunc U( Element of ( Open_Domains_of T), Element of ( Open_Domains_of T)) = ($1 /\ $2);

        thus for o1,o2 be BinOp of ( Open_Domains_of T) st (for a,b be Element of ( Open_Domains_of T) holds (o1 . (a,b)) = U(a,b)) & (for a,b be Element of ( Open_Domains_of T) holds (o2 . (a,b)) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    notation

      let T be TopSpace;

      synonym OPD-Meet T for Open_Domains_Meet T;

    end

    theorem :: TDLAT_1:37

    

     Th37: for A,B be Element of ( Open_Domains_of T) holds (( OPD-Meet T) . (A,B)) = (( D-Meet T) . (A,B))

    proof

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

      

       A1: A in { D where D be Subset of T : D is open_condensed };

      ( Open_Domains_of T) c= ( Domains_of T) by Th35;

      then

      reconsider A0 = A, B0 = B as Element of ( Domains_of T);

      B in { E where E be Subset of T : E is open_condensed };

      then

      consider E be Subset of T such that

       A2: E = B and

       A3: E is open_condensed;

      consider D be Subset of T such that

       A4: D = A and

       A5: D is open_condensed by A1;

      (D /\ E) is open_condensed by A5, A3, TOPS_1: 69;

      then (A /\ B) is condensed by A4, A2, TOPS_1: 67;

      then

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

      

      thus (( OPD-Meet T) . (A,B)) = (A /\ B) by Def11

      .= (( Cl ( Int (A0 /\ B0))) /\ (A0 /\ B0)) by A6, XBOOLE_1: 28

      .= (( D-Meet T) . (A,B)) by Def3;

    end;

    theorem :: TDLAT_1:38

    

     Th38: for T be TopSpace holds LattStr (# ( Open_Domains_of T), ( OPD-Union T), ( OPD-Meet T) #) is B_Lattice

    proof

      let T be TopSpace;

      set L = LattStr (# ( Open_Domains_of T), ( OPD-Union T), ( OPD-Meet T) #);

      

       A1: L is join-commutative

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Open_Domains_of T);

        

        thus (a "\/" b) = ( Int ( Cl (B \/ A))) by Def10

        .= (b "\/" a) by Def10;

      end;

      

       A2: L is meet-absorbing

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Open_Domains_of T);

        B in { D where D be Subset of T : D is open_condensed };

        then

         A3: ex D be Subset of T st D = B & D is open_condensed;

        (a "/\" b) = (A /\ B) by Def11;

        

        hence ((a "/\" b) "\/" b) = ( Int ( Cl ((A /\ B) \/ B))) by Def10

        .= ( Int ( Cl B)) by XBOOLE_1: 22

        .= b by A3, TOPS_1:def 8;

      end;

      

       A4: L is join-absorbing

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Open_Domains_of T);

        

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

        A in { D where D be Subset of T : D is open_condensed };

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

        then

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

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

        then

         A7: (A \/ ( Int ( Cl B))) c= ( Int ( Cl (A \/ B))) by A6, TOPS_1: 20;

        (a "\/" b) = ( Int ( Cl (A \/ B))) by Def10;

        

        hence (a "/\" (a "\/" b)) = (A /\ ( Int ( Cl (A \/ B)))) by Def11

        .= a by A5, A7, XBOOLE_1: 1, XBOOLE_1: 28;

      end;

      

       A8: L is meet-associative

      proof

        let a,b,c be Element of L;

        reconsider A = a, B = b, C = c as Element of ( Open_Domains_of T);

        

         A9: (a "/\" b) = (A /\ B) by Def11;

        (b "/\" c) = (B /\ C) by Def11;

        

        hence (a "/\" (b "/\" c)) = (A /\ (B /\ C)) by Def11

        .= ((A /\ B) /\ C) by XBOOLE_1: 16

        .= ((a "/\" b) "/\" c) by A9, Def11;

      end;

      

       A10: L is join-associative

      proof

        let a,b,c be Element of L;

        reconsider A = a, B = b, C = c as Element of ( Open_Domains_of T);

        A in { D where D be Subset of T : D is open_condensed };

        then

         A11: ex D be Subset of T st D = A & D is open_condensed;

        B in { E where E be Subset of T : E is open_condensed };

        then

         A12: ex E be Subset of T st E = B & E is open_condensed;

        C in { F where F be Subset of T : F is open_condensed };

        then

         A13: ex F be Subset of T st F = C & F is open_condensed;

        

         A14: (a "\/" b) = ( Int ( Cl (A \/ B))) by Def10;

        (b "\/" c) = ( Int ( Cl (B \/ C))) by Def10;

        

        hence (a "\/" (b "\/" c)) = ( Int ( Cl (A \/ ( Int ( Cl (B \/ C)))))) by Def10

        .= ( Int ( Cl (( Int ( Cl (A \/ B))) \/ C))) by A11, A12, A13, Th29

        .= ((a "\/" b) "\/" c) by A14, Def10;

      end;

      L is meet-commutative

      proof

        let a,b be Element of L;

        reconsider A = a, B = b as Element of ( Open_Domains_of T);

        

        thus (a "/\" b) = (B /\ A) by Def11

        .= (b "/\" a) by Def11;

      end;

      then

      reconsider L as Lattice by A1, A10, A2, A8, A4;

      

       A15: L is upper-bounded

      proof

        

         A16: ( [#] T) is open_condensed by Th21;

        then ( [#] T) in { D where D be Subset of T : D is open_condensed };

        then

        reconsider c = ( [#] T) as Element of L;

        take c;

        let a be Element of L;

        reconsider C = c, A = a as Element of ( Open_Domains_of T);

        

        thus (c "\/" a) = ( Int ( Cl (C \/ A))) by Def10

        .= ( Int ( Cl C)) by XBOOLE_1: 12

        .= c by A16, TOPS_1:def 8;

        hence (a "\/" c) = c;

      end;

      

       A17: L is distributive

      proof

        let a,b,c be Element of L;

        reconsider A = a, B = b, C = c as Element of ( Open_Domains_of T);

        A in { D where D be Subset of T : D is open_condensed };

        then

        consider D be Subset of T such that

         A18: D = A and

         A19: D is open_condensed;

        

         A20: D is open by A19, TOPS_1: 67;

        

         A21: (a "/\" c) = (A /\ C) by Def11;

        C in { F where F be Subset of T : F is open_condensed };

        then

        consider F be Subset of T such that

         A22: F = C and F is open_condensed;

        B in { E where E be Subset of T : E is open_condensed };

        then

        consider E be Subset of T such that

         A23: E = B and E is open_condensed;

        

         A24: (a "/\" b) = (A /\ B) by Def11;

        (b "\/" c) = ( Int ( Cl (B \/ C))) by Def10;

        

        hence (a "/\" (b "\/" c)) = (A /\ ( Int ( Cl (B \/ C)))) by Def11

        .= (( Int ( Cl A)) /\ ( Int ( Cl (B \/ C)))) by A18, A19, TOPS_1:def 8

        .= ( Int ( Cl (D /\ (E \/ F)))) by A18, A23, A22, A20, Th7

        .= ( Int ( Cl ((A /\ B) \/ (A /\ C)))) by A18, A23, A22, XBOOLE_1: 23

        .= ((a "/\" b) "\/" (a "/\" c)) by A24, A21, Def10;

      end;

      

       A25: L is complemented

      proof

        ( [#] T) is open_condensed by Th21;

        then ( [#] T) in { K where K be Subset of T : K is open_condensed };

        then

        reconsider c = ( [#] T) as Element of L;

        let b be Element of L;

        reconsider B = b as Element of ( Open_Domains_of T);

        B in { D where D be Subset of T : D is open_condensed };

        then

        consider D be Subset of T such that

         A26: D = B and

         A27: D is open_condensed;

        

         A28: D is open by A27, TOPS_1: 67;

        D is condensed by A27, TOPS_1: 67;

        then ( Int (B ` )) is open_condensed by A26, Th16, Th25;

        then ( Int (B ` )) in { K where K be Subset of T : K is open_condensed };

        then

        reconsider a = ( Int (B ` )) as Element of L;

        take a;

        

         A29: (B ` ) misses B by XBOOLE_1: 79;

        

         A30: for v be Element of L holds (the L_meet of L . (c,v)) = v

        proof

          let v be Element of L;

          reconsider V = v as Element of ( Open_Domains_of T);

          

          thus (the L_meet of L . (c,v)) = (( [#] T) /\ V) by Def11

          .= v by XBOOLE_1: 28;

        end;

        

        thus (a "\/" b) = ( Int ( Cl (B \/ ( Int (B ` ))))) by Def10

        .= ( Int ( [#] T)) by Th9

        .= c by TOPS_1: 15

        .= ( Top L) by A30, LATTICE2: 17;

        hence (b "\/" a) = ( Top L);

        ( {} T) is open_condensed by Th20;

        then ( {} T) in { K where K be Subset of T : K is open_condensed };

        then

        reconsider c = ( {} T) as Element of L;

        

         A31: for v be Element of L holds (the L_join of L . (c,v)) = v

        proof

          let v be Element of L;

          reconsider V = v as Element of ( Open_Domains_of T);

          V in { K where K be Subset of T : K is open_condensed };

          then

           A32: ex D be Subset of T st D = V & D is open_condensed;

          

          thus (the L_join of L . (c,v)) = ( Int ( Cl (( {} T) \/ V))) by Def10

          .= ( Int ( Cl ((( [#] T) ` ) \/ ((V ` ) ` )))) by XBOOLE_1: 37

          .= ( Int ( Cl ((( [#] T) /\ (V ` )) ` ))) by XBOOLE_1: 54

          .= ( Int ( Cl ((V ` ) ` ))) by XBOOLE_1: 28

          .= v by A32, TOPS_1:def 8;

        end;

        

        thus (a "/\" b) = (( Int (B ` )) /\ B) by Def11

        .= (( Int (D ` )) /\ ( Int D)) by A26, A28, TOPS_1: 23

        .= ( Int ((B ` ) /\ B)) by A26, TOPS_1: 17

        .= ( Int ( {} T)) by A29

        .= ( Bottom L) by A31, LATTICE2: 15;

        hence (b "/\" a) = ( Bottom L);

      end;

      L is lower-bounded

      proof

        ( {} T) is open_condensed by Th20;

        then ( {} T) in { D where D be Subset of T : D is open_condensed };

        then

        reconsider c = ( {} T) as Element of L;

        take c;

        let a be Element of L;

        reconsider C = c, A = a as Element of ( Open_Domains_of T);

        

        thus (c "/\" a) = (C /\ A) by Def11

        .= c;

        hence (a "/\" c) = c;

      end;

      hence thesis by A15, A25, A17;

    end;

    definition

      let T be TopSpace;

      :: TDLAT_1:def12

      func Open_Domains_Lattice T -> B_Lattice equals LattStr (# ( Open_Domains_of T), ( Open_Domains_Union T), ( Open_Domains_Meet T) #);

      coherence by Th38;

    end

    begin

    theorem :: TDLAT_1:39

    

     Th39: ( CLD-Union T) = (( D-Union T) || ( Closed_Domains_of T))

    proof

      

       A1: ( Closed_Domains_of T) c= ( Domains_of T) by Th31;

      then

      reconsider F = ( CLD-Union T) as Function of [:( Closed_Domains_of T), ( Closed_Domains_of T):], ( Domains_of T) by FUNCT_2: 7;

       [:( Closed_Domains_of T), ( Closed_Domains_of T):] c= [:( Domains_of T), ( Domains_of T):] by A1, ZFMISC_1: 96;

      then

      reconsider G = (( D-Union T) || ( Closed_Domains_of T)) as Function of [:( Closed_Domains_of T), ( Closed_Domains_of T):], ( Domains_of T) by FUNCT_2: 32;

      for A be Element of ( Closed_Domains_of T), B be Element of ( Closed_Domains_of T) holds (F . (A,B)) = (G . (A,B))

      proof

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

        

        thus (F . (A,B)) = (( D-Union T) . (A,B)) by Th32

        .= ((( D-Union T) || ( Closed_Domains_of T)) . [A, B]) by FUNCT_1: 49

        .= (G . (A,B));

      end;

      hence thesis by BINOP_1: 2;

    end;

    theorem :: TDLAT_1:40

    

     Th40: ( CLD-Meet T) = (( D-Meet T) || ( Closed_Domains_of T))

    proof

      

       A1: ( Closed_Domains_of T) c= ( Domains_of T) by Th31;

      then

      reconsider F = ( CLD-Meet T) as Function of [:( Closed_Domains_of T), ( Closed_Domains_of T):], ( Domains_of T) by FUNCT_2: 7;

       [:( Closed_Domains_of T), ( Closed_Domains_of T):] c= [:( Domains_of T), ( Domains_of T):] by A1, ZFMISC_1: 96;

      then

      reconsider G = (( D-Meet T) || ( Closed_Domains_of T)) as Function of [:( Closed_Domains_of T), ( Closed_Domains_of T):], ( Domains_of T) by FUNCT_2: 32;

      for A be Element of ( Closed_Domains_of T), B be Element of ( Closed_Domains_of T) holds (F . (A,B)) = (G . (A,B))

      proof

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

        

        thus (F . (A,B)) = (( D-Meet T) . (A,B)) by Th33

        .= ((( D-Meet T) || ( Closed_Domains_of T)) . [A, B]) by FUNCT_1: 49

        .= (G . (A,B));

      end;

      hence thesis by BINOP_1: 2;

    end;

    theorem :: TDLAT_1:41

    ( Closed_Domains_Lattice T) is SubLattice of ( Domains_Lattice T)

    proof

      set L = ( Domains_Lattice T), CL = ( Closed_Domains_Lattice T);

      thus the carrier of CL c= the carrier of L by Th31;

      thus the L_join of CL = (the L_join of L || the carrier of CL) by Th39;

      thus thesis by Th40;

    end;

    theorem :: TDLAT_1:42

    

     Th42: ( OPD-Union T) = (( D-Union T) || ( Open_Domains_of T))

    proof

      

       A1: ( Open_Domains_of T) c= ( Domains_of T) by Th35;

      then

      reconsider F = ( OPD-Union T) as Function of [:( Open_Domains_of T), ( Open_Domains_of T):], ( Domains_of T) by FUNCT_2: 7;

       [:( Open_Domains_of T), ( Open_Domains_of T):] c= [:( Domains_of T), ( Domains_of T):] by A1, ZFMISC_1: 96;

      then

      reconsider G = (( D-Union T) || ( Open_Domains_of T)) as Function of [:( Open_Domains_of T), ( Open_Domains_of T):], ( Domains_of T) by FUNCT_2: 32;

      for A be Element of ( Open_Domains_of T), B be Element of ( Open_Domains_of T) holds (F . (A,B)) = (G . (A,B))

      proof

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

        

        thus (F . (A,B)) = (( D-Union T) . (A,B)) by Th36

        .= ((( D-Union T) || ( Open_Domains_of T)) . [A, B]) by FUNCT_1: 49

        .= (G . (A,B));

      end;

      hence thesis by BINOP_1: 2;

    end;

    theorem :: TDLAT_1:43

    

     Th43: ( OPD-Meet T) = (( D-Meet T) || ( Open_Domains_of T))

    proof

      

       A1: ( Open_Domains_of T) c= ( Domains_of T) by Th35;

      then

      reconsider F = ( OPD-Meet T) as Function of [:( Open_Domains_of T), ( Open_Domains_of T):], ( Domains_of T) by FUNCT_2: 7;

       [:( Open_Domains_of T), ( Open_Domains_of T):] c= [:( Domains_of T), ( Domains_of T):] by A1, ZFMISC_1: 96;

      then

      reconsider G = (( D-Meet T) || ( Open_Domains_of T)) as Function of [:( Open_Domains_of T), ( Open_Domains_of T):], ( Domains_of T) by FUNCT_2: 32;

      for A be Element of ( Open_Domains_of T), B be Element of ( Open_Domains_of T) holds (F . (A,B)) = (G . (A,B))

      proof

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

        

        thus (F . (A,B)) = (( D-Meet T) . (A,B)) by Th37

        .= ((( D-Meet T) || ( Open_Domains_of T)) . [A, B]) by FUNCT_1: 49

        .= (G . (A,B));

      end;

      hence thesis by BINOP_1: 2;

    end;

    theorem :: TDLAT_1:44

    ( Open_Domains_Lattice T) is SubLattice of ( Domains_Lattice T)

    proof

      set L = ( Domains_Lattice T), OL = ( Open_Domains_Lattice T);

      thus the carrier of OL c= the carrier of L by Th35;

      thus the L_join of OL = (the L_join of L || the carrier of OL) by Th42;

      thus thesis by Th43;

    end;