tops_3.miz

    begin

    reserve X for TopStruct,

A for Subset of X;

    theorem :: TOPS_3:1



     Th1: (A = ( {} X) iff (A ` ) = ( [#] X)) & (A = {} iff (A ` ) = the carrier of X)

    proof

      thus A = ( {} X) iff (A ` ) = ( [#] X)

      proof

        thus A = ( {} X) implies (A ` ) = ( [#] X);

        assume (A ` ) = ( [#] X);

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

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TOPS_3:2



     Th2: (A = ( [#] X) iff (A ` ) = ( {} X)) & (A = the carrier of X iff (A ` ) = {} ) by XBOOLE_1: 37;

    theorem :: TOPS_3:3



     Th3: for X be TopSpace, A,B be Subset of X holds (( Int A) /\ ( Cl B)) c= ( Cl (A /\ B))

    proof

      let X be TopSpace, A,B be Subset of X;

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

      then

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

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

      hence thesis by A1, XBOOLE_1: 1;

    end;

    reserve X for TopSpace,

A,B for Subset of X;

    theorem :: TOPS_3:4



     Th4: ( Int (A \/ B)) c= (( Cl A) \/ ( Int B))

    proof

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

      then (( Cl ((A ` ) /\ (B ` ))) ` ) c= ((( Int (A ` )) /\ ( Cl (B ` ))) ` ) by SUBSET_1: 12;

      then ( Int (((A ` ) /\ (B ` )) ` )) c= ((( Int (A ` )) /\ ( Cl (B ` ))) ` ) by TDLAT_3: 3;

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

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

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

      hence thesis by TOPS_1:def 1;

    end;

    theorem :: TOPS_3:5



     Th5: for A be Subset of X st A is closed holds ( Int (A \/ B)) c= (A \/ ( Int B))

    proof

      let A be Subset of X;

      assume A is closed;

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

      hence thesis by Th4;

    end;

    theorem :: TOPS_3:6



     Th6: for A be Subset of X st A is closed holds ( Int (A \/ B)) = ( Int (A \/ ( Int B)))

    proof

      let A be Subset of X;

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

      then

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

      assume A is closed;

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

      hence thesis by A1;

    end;

    theorem :: TOPS_3:7



     Th7: A misses ( Int ( Cl A)) implies ( Int ( Cl A)) = {}

    proof

      reconsider A9 = A as Subset of X;

      assume (A /\ ( Int ( Cl A))) = {} ;

      then A9 misses ( Int ( Cl A9));

      then ( Cl A) misses ( Int ( Cl A)) by TSEP_1: 36;

      then (( Cl A) /\ ( Int ( Cl A))) = {} ;

      hence thesis by TOPS_1: 16, XBOOLE_1: 28;

    end;

    theorem :: TOPS_3:8

    (A \/ ( Cl ( Int A))) = the carrier of X implies ( Cl ( Int A)) = the carrier of X

    proof

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

      then (( Int A) \/ ( Cl ( Int A))) = the carrier of X by TDLAT_3: 4;

      hence thesis by PRE_TOPC: 18, XBOOLE_1: 12;

    end;

    begin

    definition

      let X be TopStruct, A be Subset of X;

      :: original: boundary

      redefine

      :: TOPS_3:def1

      attr A is boundary means

      : Def1: ( Int A) = {} ;

      compatibility by TOPS_1: 48;

    end

    theorem :: TOPS_3:9

    ( {} X) is boundary;

    reserve X for non empty TopSpace,

A for Subset of X;

    theorem :: TOPS_3:10



     Th10: A is boundary implies A <> the carrier of X

    proof

      assume

       A1: ( Int A) = {} ;

      assume A = the carrier of X;

      then A = ( [#] X);

      hence contradiction by A1, TOPS_1: 15;

    end;

    reserve X for TopSpace,

A,B for Subset of X;

    theorem :: TOPS_3:11



     Th11: B is boundary & A c= B implies A is boundary by TOPS_1: 19, XBOOLE_1: 3;

    theorem :: TOPS_3:12

    A is boundary iff for C be Subset of X st (A ` ) c= C & C is closed holds C = the carrier of X

    proof

      thus A is boundary implies for C be Subset of X st (A ` ) c= C & C is closed holds C = the carrier of X

      proof

        assume

         A1: A is boundary;

        let C be Subset of X;

        assume (A ` ) c= C;

        then

         A2: (C ` ) c= ((A ` ) ` ) by SUBSET_1: 12;

        assume C is closed;

        then (C ` ) = ( {} X) by A1, A2, TOPS_1: 50;

        hence thesis by Th2;

      end;

      assume

       A3: for C be Subset of X st (A ` ) c= C & C is closed holds C = the carrier of X;

      now

        let G be Subset of X;

        assume that

         A4: G c= A and

         A5: G is open;

        (A ` ) c= (G ` ) by A4, SUBSET_1: 12;

        then (G ` ) = the carrier of X by A3, A5;

        hence G = {} by Th1;

      end;

      hence thesis by TOPS_1: 50;

    end;

    theorem :: TOPS_3:13

    A is boundary iff for G be Subset of X st G <> {} & G is open holds (A ` ) meets G

    proof

      thus A is boundary implies for G be Subset of X st G <> {} & G is open holds (A ` ) meets G by SUBSET_1: 24, TOPS_1: 50;

      assume

       A1: for G be Subset of X st G <> {} & G is open holds (A ` ) meets G;

      assume ( Int A) <> {} ;

      then ( Int A) c= A & (A ` ) meets ( Int A) by A1, TOPS_1: 16;

      hence contradiction by SUBSET_1: 24;

    end;

    theorem :: TOPS_3:14

    A is boundary iff for F be Subset of X holds F is closed implies ( Int F) = ( Int (F \/ A))

    proof

      thus A is boundary implies for F be Subset of X holds F is closed implies ( Int F) = ( Int (F \/ A))

      proof

        assume

         A1: ( Int A) = {} ;

        let F be Subset of X;

        assume F is closed;

        then ( Int (F \/ A)) = ( Int (F \/ ( Int A))) by Th6;

        hence thesis by A1;

      end;

      assume for F be Subset of X holds F is closed implies ( Int F) = ( Int (F \/ A));

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

      hence thesis;

    end;

    theorem :: TOPS_3:15

    A is boundary implies (A /\ B) is boundary by Th11, XBOOLE_1: 17;

    definition

      let X be TopStruct, A be Subset of X;

      :: original: dense

      redefine

      :: TOPS_3:def2

      attr A is dense means ( Cl A) = the carrier of X;

      compatibility

      proof

        thus A is dense implies ( Cl A) = the carrier of X

        proof

          assume A is dense;

          then ( Cl A) = ( [#] X) by TOPS_1:def 3;

          hence thesis;

        end;

        assume ( Cl A) = the carrier of X;

        then ( Cl A) = ( [#] X);

        hence thesis by TOPS_1:def 3;

      end;

    end

    theorem :: TOPS_3:16

    ( [#] X) is dense;

    reserve X for non empty TopSpace,

A,B for Subset of X;

    theorem :: TOPS_3:17



     Th17: A is dense implies A <> {}

    proof

      assume A is dense;

      then

       A1: ( Cl A) = ( [#] X);

      assume A = {} ;

      hence contradiction by A1, PRE_TOPC: 22;

    end;

    theorem :: TOPS_3:18



     Th18: A is dense iff (A ` ) is boundary

    proof

      thus A is dense implies (A ` ) is boundary

      proof

        assume A is dense;

        then ((A ` ) ` ) is dense;

        hence thesis by TOPS_1:def 4;

      end;

      assume (A ` ) is boundary;

      then ((A ` ) ` ) is dense by TOPS_1:def 4;

      hence thesis;

    end;

    theorem :: TOPS_3:19

    A is dense iff for C be Subset of X st A c= C & C is closed holds C = the carrier of X by TOPS_1: 5, PRE_TOPC: 18;

    theorem :: TOPS_3:20

    A is dense iff for G be Subset of X holds G is open implies ( Cl G) = ( Cl (G /\ A))

    proof

      thus A is dense implies for G be Subset of X holds G is open implies ( Cl G) = ( Cl (G /\ A))

      proof

        assume

         A1: A is dense;

        let G be Subset of X;

        assume G is open;

        then

         A2: ( Cl (G /\ ( Cl A))) = ( Cl (G /\ A)) by TOPS_1: 14;

        (G /\ ( [#] X)) = G by XBOOLE_1: 28;

        hence thesis by A1, A2;

      end;

      assume for G be Subset of X holds G is open implies ( Cl G) = ( Cl (G /\ A));

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

      then

       A3: ( [#] X) = ( Cl (( [#] X) /\ A)) by TOPS_1: 2;

      (( [#] X) /\ A) = A by XBOOLE_1: 28;

      hence thesis by A3;

    end;

    theorem :: TOPS_3:21

    A is dense implies (A \/ B) is dense by TOPS_1: 44, XBOOLE_1: 7;

    definition

      let X be TopStruct, A be Subset of X;

      :: original: nowhere_dense

      redefine

      :: TOPS_3:def3

      attr A is nowhere_dense means ( Int ( Cl A)) = {} ;

      compatibility by Def1, TOPS_1:def 5;

    end

    theorem :: TOPS_3:22

    ( {} X) is nowhere_dense;

    theorem :: TOPS_3:23

    A is nowhere_dense implies A <> the carrier of X by Th10;

    theorem :: TOPS_3:24

    A is nowhere_dense implies ( Cl A) is nowhere_dense;

    theorem :: TOPS_3:25

    A is nowhere_dense implies not A is dense

    proof

      assume

       A1: ( Int ( Cl A)) = {} ;

      assume A is dense;

      then ( Cl A) = ( [#] X);

      hence contradiction by A1, TOPS_1: 15;

    end;

    theorem :: TOPS_3:26



     Th26: B is nowhere_dense & A c= B implies A is nowhere_dense

    proof

      assume B is nowhere_dense;

      then

       A1: ( Cl B) is boundary;

      assume A c= B;

      then ( Cl A) is boundary by A1, Th11, PRE_TOPC: 19;

      hence thesis;

    end;

    theorem :: TOPS_3:27



     Th27: A is nowhere_dense iff ex C be Subset of X st A c= C & C is closed & C is boundary

    proof

      thus A is nowhere_dense implies ex C be Subset of X st A c= C & C is closed & C is boundary

      proof

        assume

         A1: A is nowhere_dense;

        take ( Cl A);

        thus thesis by A1, PRE_TOPC: 18;

      end;

      given C be Subset of X such that

       A2: A c= C & C is closed & C is boundary;

      ( Cl A) is boundary by A2, Th11, TOPS_1: 5;

      hence thesis;

    end;

    theorem :: TOPS_3:28



     Th28: A is nowhere_dense iff for G be Subset of X st G <> {} & G is open holds ex H be Subset of X st H c= G & H <> {} & H is open & A misses H

    proof

      thus A is nowhere_dense implies for G be Subset of X st G <> {} & G is open holds ex H be Subset of X st H c= G & H <> {} & H is open & A misses H

      proof

        assume A is nowhere_dense;

        then

         A1: ( Cl A) is boundary;

        let G be Subset of X;

        assume G <> {} & G is open;

        then

        consider H be Subset of X such that

         A2: H c= G & H <> {} & H is open & ( Cl A) misses H by A1, TOPS_1: 51;

        take H;

        thus thesis by A2, PRE_TOPC: 18, XBOOLE_1: 63;

      end;

      assume

       A3: for G be Subset of X st G <> {} & G is open holds ex H be Subset of X st H c= G & H <> {} & H is open & A misses H;

      for G be Subset of X st G <> {} & G is open holds ex H be Subset of X st H c= G & H <> {} & H is open & ( Cl A) misses H

      proof

        let G be Subset of X;

        assume G <> {} & G is open;

        then

        consider H be Subset of X such that

         A4: H c= G & H <> {} & H is open & A misses H by A3;

        take H;

        thus thesis by A4, TSEP_1: 36;

      end;

      then ( Cl A) is boundary by TOPS_1: 51;

      hence thesis;

    end;

    theorem :: TOPS_3:29

    A is nowhere_dense implies (A /\ B) is nowhere_dense by Th26, XBOOLE_1: 17;

    theorem :: TOPS_3:30



     Th30: A is nowhere_dense & B is boundary implies (A \/ B) is boundary

    proof

      assume A is nowhere_dense;

      then

       A1: ( Cl A) is boundary;

      assume B is boundary;

      then A c= ( Cl A) & (B \/ ( Cl A)) is boundary by A1, PRE_TOPC: 18, TOPS_1: 49;

      hence thesis by Th11, XBOOLE_1: 9;

    end;

    definition

      let X be TopStruct, A be Subset of X;

      :: TOPS_3:def4

      attr A is everywhere_dense means ( Cl ( Int A)) = ( [#] X);

    end

    definition

      let X be TopStruct, A be Subset of X;

      :: original: everywhere_dense

      redefine

      :: TOPS_3:def5

      attr A is everywhere_dense means ( Cl ( Int A)) = the carrier of X;

      compatibility ;

    end

    theorem :: TOPS_3:31

    ( [#] X) is everywhere_dense

    proof

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

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

      hence thesis;

    end;

    theorem :: TOPS_3:32

    A is everywhere_dense implies ( Int A) is everywhere_dense;

    theorem :: TOPS_3:33



     Th33: A is everywhere_dense implies A is dense

    proof

      assume A is everywhere_dense;

      then ( Cl ( Int A)) = ( [#] X);

      then ( [#] X) c= ( Cl A) by PRE_TOPC: 19, TOPS_1: 16;

      then ( Cl A) = ( [#] X);

      hence thesis;

    end;

    theorem :: TOPS_3:34

    A is everywhere_dense implies A <> {} by Th17, Th33;

    theorem :: TOPS_3:35

    A is everywhere_dense iff ( Int A) is dense;

    theorem :: TOPS_3:36



     Th36: A is open & A is dense implies A is everywhere_dense by TOPS_1: 23;

    theorem :: TOPS_3:37

    A is everywhere_dense implies not A is boundary by PRE_TOPC: 22;

    theorem :: TOPS_3:38



     Th38: A is everywhere_dense & A c= B implies B is everywhere_dense

    proof

      assume A is everywhere_dense;

      then

       A1: ( Cl ( Int A)) = ( [#] X);

      assume A c= B;

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

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

      then ( [#] X) = ( Cl ( Int B)) by A1;

      hence thesis;

    end;

    theorem :: TOPS_3:39



     Th39: A is everywhere_dense iff (A ` ) is nowhere_dense

    proof

      thus A is everywhere_dense implies (A ` ) is nowhere_dense

      proof

        assume A is everywhere_dense;

        then ( Cl ( Int A)) = ( [#] X);

        then (( Cl ( Int A)) ` ) = ( {} X) by Th2;

        then ( Int (( Int A) ` )) = ( {} X) by TDLAT_3: 3;

        then ( Int ( Cl (A ` ))) = {} by TDLAT_3: 2;

        then ( Cl (A ` )) is boundary;

        hence thesis;

      end;

      assume (A ` ) is nowhere_dense;

      then ( Cl (A ` )) is boundary;

      then ( Int ( Cl (A ` ))) = ( {} X);

      then ( Int (( Int A) ` )) = ( {} X) by TDLAT_3: 2;

      then (( Cl ( Int A)) ` ) = ( {} X) by TDLAT_3: 3;

      then ( Cl ( Int A)) = ( [#] X) by Th2;

      hence thesis;

    end;

    theorem :: TOPS_3:40



     Th40: A is nowhere_dense iff (A ` ) is everywhere_dense

    proof

      thus A is nowhere_dense implies (A ` ) is everywhere_dense

      proof

        assume A is nowhere_dense;

        then ( Cl A) is boundary;

        then ( Int ( Cl A)) = ( {} X);

        then ( Int (( Int (A ` )) ` )) = ( {} X) by TDLAT_3: 1;

        then (( Cl ( Int (A ` ))) ` ) = ( {} X) by TDLAT_3: 3;

        then ( Cl ( Int (A ` ))) = ( [#] X) by Th2;

        hence thesis;

      end;

      assume (A ` ) is everywhere_dense;

      then ( Cl ( Int (A ` ))) = ( [#] X);

      then (( Cl ( Int (A ` ))) ` ) = ( {} X) by Th2;

      then ( Int (( Int (A ` )) ` )) = ( {} X) by TDLAT_3: 3;

      then ( Int ( Cl A)) = {} by TDLAT_3: 1;

      then ( Cl A) is boundary;

      hence thesis;

    end;

    theorem :: TOPS_3:41



     Th41: A is everywhere_dense iff ex C be Subset of X st C c= A & C is open & C is dense

    proof

      thus A is everywhere_dense implies ex C be Subset of X st C c= A & C is open & C is dense

      proof

        assume

         A1: A is everywhere_dense;

        take ( Int A);

        thus thesis by A1, TOPS_1: 16;

      end;

      given C be Subset of X such that

       A2: C c= A & C is open & C is dense;

      ( Int A) is dense by A2, TOPS_1: 24, TOPS_1: 44;

      hence thesis;

    end;

    theorem :: TOPS_3:42

    A is everywhere_dense iff for F be Subset of X st F <> the carrier of X & F is closed holds ex H be Subset of X st F c= H & H <> the carrier of X & H is closed & (A \/ H) = the carrier of X

    proof

      thus A is everywhere_dense implies for F be Subset of X st F <> the carrier of X & F is closed holds ex H be Subset of X st F c= H & H <> the carrier of X & H is closed & (A \/ H) = the carrier of X

      proof

        assume A is everywhere_dense;

        then

         A1: (A ` ) is nowhere_dense by Th39;

        let F be Subset of X;

        assume F <> the carrier of X;

        then

         A2: (( [#] X) \ F) <> {} by PRE_TOPC: 4;

        assume F is closed;

        then

        consider G be Subset of X such that

         A3: G c= (F ` ) and

         A4: G <> {} and

         A5: G is open and

         A6: (A ` ) misses G by A1, A2, Th28;

        take H = (G ` );

        ((F ` ) ` ) c= H by A3, SUBSET_1: 12;

        hence F c= H;

        (H ` ) <> {} by A4;

        then (( [#] X) \ H) <> {} ;

        hence H <> the carrier of X by PRE_TOPC: 4;

        thus H is closed by A5;

        ((A ` ) /\ (H ` )) = {} by A6;

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

        hence thesis by Th2;

      end;

      assume

       A7: for F be Subset of X st F <> the carrier of X & F is closed holds ex H be Subset of X st F c= H & H <> the carrier of X & H is closed & (A \/ H) = the carrier of X;

      for G be Subset of X st G <> {} & G is open holds ex H be Subset of X st H c= G & H <> {} & H is open & (A ` ) misses H

      proof

        let G be Subset of X;

        assume G <> {} ;

        then ((G ` ) ` ) <> {} ;

        then

         A8: (G ` ) <> ( [#] X) by PRE_TOPC: 4;

        assume G is open;

        then

        consider F be Subset of X such that

         A9: (G ` ) c= F and

         A10: F <> the carrier of X and

         A11: F is closed and

         A12: (A \/ F) = the carrier of X by A7, A8;

        take H = (F ` );

        H c= ((G ` ) ` ) by A9, SUBSET_1: 12;

        hence H c= G;

        F <> ( [#] X) by A10;

        hence H <> {} by PRE_TOPC: 4;

        thus H is open by A11;

        ((A \/ F) ` ) = ( {} X) by A12, Th2;

        hence ((A ` ) /\ H) = {} by XBOOLE_1: 53;

      end;

      then (A ` ) is nowhere_dense by Th28;

      hence thesis by Th39;

    end;

    theorem :: TOPS_3:43

    A is everywhere_dense implies (A \/ B) is everywhere_dense by Th38, XBOOLE_1: 7;

    theorem :: TOPS_3:44



     Th44: A is everywhere_dense & B is everywhere_dense implies (A /\ B) is everywhere_dense

    proof

      assume A is everywhere_dense & B is everywhere_dense;

      then (A ` ) is nowhere_dense & (B ` ) is nowhere_dense by Th39;

      then ((A ` ) \/ (B ` )) = ((A /\ B) ` ) & ((A ` ) \/ (B ` )) is nowhere_dense by TOPS_1: 53, XBOOLE_1: 54;

      hence thesis by Th39;

    end;

    theorem :: TOPS_3:45



     Th45: A is everywhere_dense & B is dense implies (A /\ B) is dense

    proof

      assume A is everywhere_dense;

      then

       A1: (A ` ) is nowhere_dense by Th39;

      assume B is dense;

      then (B ` ) is boundary by Th18;

      then ((A ` ) \/ (B ` )) = ((A /\ B) ` ) & ((A ` ) \/ (B ` )) is boundary by A1, Th30, XBOOLE_1: 54;

      hence thesis by Th18;

    end;

    theorem :: TOPS_3:46

    A is dense & B is nowhere_dense implies (A \ B) is dense

    proof

      assume

       A1: A is dense;



       A2: (A \ B) = ((B ` ) /\ A) by SUBSET_1: 13;

      assume B is nowhere_dense;

      then (B ` ) is everywhere_dense by Th40;

      hence thesis by A1, A2, Th45;

    end;

    theorem :: TOPS_3:47

    A is everywhere_dense & B is boundary implies (A \ B) is dense

    proof

      assume

       A1: A is everywhere_dense;



       A2: (A \ B) = (A /\ (B ` )) by SUBSET_1: 13;

      assume B is boundary;

      then (B ` ) is dense by TOPS_1:def 4;

      hence thesis by A1, A2, Th45;

    end;

    theorem :: TOPS_3:48

    A is everywhere_dense & B is nowhere_dense implies (A \ B) is everywhere_dense

    proof

      assume

       A1: A is everywhere_dense;



       A2: (A \ B) = (A /\ (B ` )) by SUBSET_1: 13;

      assume B is nowhere_dense;

      then (B ` ) is everywhere_dense by Th40;

      hence thesis by A1, A2, Th44;

    end;

    reserve D for Subset of X;

    theorem :: TOPS_3:49

    D is everywhere_dense implies ex C,B be Subset of X st C is open & C is dense & B is nowhere_dense & (C \/ B) = D & C misses B

    proof

      assume D is everywhere_dense;

      then

      consider C be Subset of X such that

       A1: C c= D and

       A2: C is open & C is dense by Th41;

      take C;

      take B = (D \ C);

      thus C is open & C is dense by A2;

      C is everywhere_dense by A2, Th36;

      then (C ` ) is nowhere_dense by Th39;

      hence B is nowhere_dense by Th26, XBOOLE_1: 33;

      thus thesis by A1, XBOOLE_1: 45, XBOOLE_1: 79;

    end;

    theorem :: TOPS_3:50

    D is everywhere_dense implies ex C,B be Subset of X st C is open & C is dense & B is closed & B is boundary & (C \/ (D /\ B)) = D & C misses B & (C \/ B) = the carrier of X

    proof

      assume D is everywhere_dense;

      then

      consider C be Subset of X such that

       A1: C c= D and

       A2: C is open & C is dense by Th41;

      take C;

      take B = (C ` );

      thus C is open & C is dense & B is closed & B is boundary by A2, Th18;



      thus (C \/ (D /\ B)) = ((C \/ D) /\ (C \/ (C ` ))) by XBOOLE_1: 24

      .= ((C \/ D) /\ ( [#] X)) by PRE_TOPC: 2

      .= (C \/ D) by XBOOLE_1: 28

      .= D by A1, XBOOLE_1: 12;

      C misses B by XBOOLE_1: 79;

      hence (C /\ B) = {} ;

      (C \/ B) = ( [#] X) by PRE_TOPC: 2;

      hence thesis;

    end;

    theorem :: TOPS_3:51

    D is nowhere_dense implies ex C,B be Subset of X st C is closed & C is boundary & B is everywhere_dense & (C /\ B) = D & (C \/ B) = the carrier of X

    proof

      assume D is nowhere_dense;

      then

      consider C be Subset of X such that

       A1: D c= C and

       A2: C is closed & C is boundary by Th27;

      take C;

      take B = (D \/ (C ` ));

      thus C is closed & C is boundary by A2;

      (C ` ) is everywhere_dense by A2, Th40;

      hence B is everywhere_dense by Th38, XBOOLE_1: 7;



       A3: C misses (C ` ) by XBOOLE_1: 79;



      thus (C /\ B) = ((C /\ D) \/ (C /\ (C ` ))) by XBOOLE_1: 23

      .= ((C /\ D) \/ ( {} X)) by A3

      .= D by A1, XBOOLE_1: 28;



      thus (C \/ B) = (D \/ (C \/ (C ` ))) by XBOOLE_1: 4

      .= (D \/ ( [#] X)) by PRE_TOPC: 2

      .= the carrier of X by XBOOLE_1: 12;

    end;

    theorem :: TOPS_3:52

    D is nowhere_dense implies ex C,B be Subset of X st C is closed & C is boundary & B is open & B is dense & (C /\ (D \/ B)) = D & C misses B & (C \/ B) = the carrier of X

    proof

      assume D is nowhere_dense;

      then

      consider C be Subset of X such that

       A1: D c= C and

       A2: C is closed & C is boundary by Th27;

      take C;

      take B = (C ` );

      thus C is closed & C is boundary & B is open & B is dense by A2;



       A3: C misses (C ` ) by XBOOLE_1: 79;



      thus (C /\ (D \/ B)) = ((C /\ D) \/ (C /\ (C ` ))) by XBOOLE_1: 23

      .= ((C /\ D) \/ ( {} X)) by A3

      .= D by A1, XBOOLE_1: 28;

      C misses B by XBOOLE_1: 79;

      hence (C /\ B) = {} ;

      (C \/ B) = ( [#] X) by PRE_TOPC: 2;

      hence thesis;

    end;

    begin

    reserve Y0 for SubSpace of X;

    theorem :: TOPS_3:53



     Th53: for A be Subset of X, B be Subset of Y0 st B c= A holds ( Cl B) c= ( Cl A)

    proof

      let A be Subset of X, B be Subset of Y0;

      assume

       A1: B c= A;

      then

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

      ( Cl B) = (( Cl D) /\ ( [#] Y0)) by PRE_TOPC: 17;

      then

       A2: ( Cl B) c= ( Cl D) by XBOOLE_1: 17;

      ( Cl D) c= ( Cl A) by A1, PRE_TOPC: 19;

      hence thesis by A2, XBOOLE_1: 1;

    end;

    theorem :: TOPS_3:54



     Th54: for C,A be Subset of X, B be Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds ( Cl A) = ( Cl B)

    proof

      let C,A be Subset of X, B be Subset of Y0;

      assume

       A1: C is closed;

      assume

       A2: C c= the carrier of Y0;

      assume A c= C;

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

      then ( Cl A) c= C by A1, PRE_TOPC: 22;

      then

       A3: ( Cl A) = (( Cl A) /\ ( [#] Y0)) by A2, XBOOLE_1: 1, XBOOLE_1: 28;

      assume A = B;

      hence thesis by A3, PRE_TOPC: 17;

    end;

    theorem :: TOPS_3:55

    for Y0 be closed non empty SubSpace of X holds for A be Subset of X, B be Subset of Y0 st A = B holds ( Cl A) = ( Cl B)

    proof

      let Y0 be closed non empty SubSpace of X;

      reconsider C = the carrier of Y0 as Subset of X by TSEP_1: 1;

      let A be Subset of X, B be Subset of Y0;



       A1: C is closed by TSEP_1: 11;

      assume A = B;

      hence thesis by A1, Th54;

    end;

    theorem :: TOPS_3:56



     Th56: for A be Subset of X, B be Subset of Y0 st A c= B holds ( Int A) c= ( Int B)

    proof

      let A be Subset of X, B be Subset of Y0;



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

      assume A c= B;

      then

       A2: ( Int A) c= B by A1, XBOOLE_1: 1;

      then

      reconsider C = ( Int A) as Subset of Y0 by XBOOLE_1: 1;

      C is open by TOPS_2: 25;

      hence thesis by A2, TOPS_1: 24;

    end;

    theorem :: TOPS_3:57



     Th57: for Y0 be non empty SubSpace of X, C,A be Subset of X, B be Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds ( Int A) = ( Int B)

    proof

      let Y0 be non empty SubSpace of X, C,A be Subset of X, B be Subset of Y0;

      assume

       A1: C is open;

      assume

       A2: C c= the carrier of Y0;

      assume

       A3: A c= C;

      assume

       A4: A = B;



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

      then

      reconsider D = ( Int B) as Subset of X by A4, XBOOLE_1: 1;

      ( Int B) c= C by A3, A4, A5, XBOOLE_1: 1;

      then D is open by A1, A2, TSEP_1: 9;

      then

       A6: D c= ( Int A) by A4, TOPS_1: 16, TOPS_1: 24;

      ( Int A) c= ( Int B) by A4, Th56;

      hence thesis by A6;

    end;

    theorem :: TOPS_3:58

    for Y0 be open non empty SubSpace of X holds for A be Subset of X, B be Subset of Y0 st A = B holds ( Int A) = ( Int B)

    proof

      let Y0 be open non empty SubSpace of X;

      reconsider C = the carrier of Y0 as Subset of X by TSEP_1: 1;

      let A be Subset of X, B be Subset of Y0;



       A1: C is open by TSEP_1: 16;

      assume A = B;

      hence thesis by A1, Th57;

    end;

    reserve X0 for SubSpace of X;

    theorem :: TOPS_3:59



     Th59: for A be Subset of X, B be Subset of X0 st A c= B holds A is dense implies B is dense

    proof

      let A be Subset of X, B be Subset of X0;



       A1: ( [#] X0) c= ( [#] X) by PRE_TOPC:def 4;

      assume

       A2: A c= B;

      then

      reconsider C = A as Subset of X0 by XBOOLE_1: 1;

      assume A is dense;

      then ( Cl A) = ( [#] X);

      then ( [#] X0) = (( Cl A) /\ ( [#] X0)) by A1, XBOOLE_1: 28;

      then ( Cl C) = ( [#] X0) by PRE_TOPC: 17;

      then C is dense;

      hence thesis by A2, TOPS_1: 44;

    end;

    theorem :: TOPS_3:60



     Th60: for C,A be Subset of X, B be Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds C is dense & B is dense iff A is dense

    proof

      let C,A be Subset of X, B be Subset of X0;

      assume

       A1: C c= the carrier of X0;

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

      assume

       A2: A c= C;

      assume

       A3: A = B;

      thus C is dense & B is dense implies A is dense

      proof

        assume C is dense;

        then ( Cl C) = ( [#] X);

        then

         A4: ( [#] X) c= ( Cl P) by A1, PRE_TOPC: 19;

        assume B is dense;

        then ( Cl B) = ( [#] X0);

        then P = (( Cl A) /\ ( [#] X0)) by A3, PRE_TOPC: 17;

        then ( Cl P) c= ( Cl ( Cl A)) by PRE_TOPC: 19, XBOOLE_1: 17;

        then ( [#] X) c= ( Cl A) by A4, XBOOLE_1: 1;

        then ( Cl A) = ( [#] X);

        hence thesis;

      end;

      thus thesis by A2, A3, Th59, TOPS_1: 44;

    end;

    reserve X0 for non empty SubSpace of X;

    theorem :: TOPS_3:61



     Th61: for A be Subset of X, B be Subset of X0 st A c= B holds A is everywhere_dense implies B is everywhere_dense

    proof

      let A be Subset of X, B be Subset of X0;

      assume

       A1: A c= B;

      then

      reconsider C = A as Subset of X0 by XBOOLE_1: 1;

      assume A is everywhere_dense;

      then ( Int A) is dense;

      then ( Int C) is dense by Th56, Th59;

      then ( Int B) is dense by A1, TOPS_1: 19, TOPS_1: 44;

      hence thesis;

    end;

    theorem :: TOPS_3:62



     Th62: for C,A be Subset of X, B be Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds C is dense & B is everywhere_dense iff A is everywhere_dense

    proof

      let C,A be Subset of X, B be Subset of X0;

      assume

       A1: C is open;

      assume C c= the carrier of X0;

      then

      reconsider E = C as Subset of X0;



       A2: E is open by A1, TOPS_2: 25;

      assume

       A3: A c= C;

      assume

       A4: A = B;



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

      then

      reconsider D = ( Int B) as Subset of X by A4, XBOOLE_1: 1;

      ( Int B) c= ( Int E) by A3, A4, TOPS_1: 19;

      then

       A6: ( Int B) c= E by A2, TOPS_1: 23;

      then

       A7: D is open by A1, TSEP_1: 9;

      thus C is dense & B is everywhere_dense implies A is everywhere_dense

      proof

        assume

         A8: C is dense;

        assume B is everywhere_dense;

        then ( Int B) is dense;

        then D is dense by A6, A8, Th60;

        then ( Int A) is dense by A4, A5, A7, TOPS_1: 24, TOPS_1: 44;

        hence thesis;

      end;

      thus A is everywhere_dense implies C is dense & B is everywhere_dense by A3, Th33, Th38, A4, Th61;

    end;

    theorem :: TOPS_3:63

    for X0 be open non empty SubSpace of X holds for A,C be Subset of X, B be Subset of X0 st C = the carrier of X0 & A = B holds C is dense & B is everywhere_dense iff A is everywhere_dense

    proof

      let X0 be open non empty SubSpace of X;

      let A,C be Subset of X, B be Subset of X0;

      assume

       A1: C = the carrier of X0;

      assume

       A2: A = B;

      C is open by A1, TSEP_1:def 1;

      hence thesis by A1, A2, Th62;

    end;

    theorem :: TOPS_3:64

    for C,A be Subset of X, B be Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds C is everywhere_dense & B is everywhere_dense iff A is everywhere_dense

    proof

      let C,A be Subset of X, B be Subset of X0;

      assume

       A1: C c= the carrier of X0;

      assume

       A2: A c= C;

      assume

       A3: A = B;

      thus C is everywhere_dense & B is everywhere_dense implies A is everywhere_dense

      proof

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

        then

        reconsider D = ( Int C) as Subset of X0 by A1, XBOOLE_1: 1;



         A4: (D /\ B) c= ( Int C) by XBOOLE_1: 17;

        then

        reconsider E = (D /\ B) as Subset of X by XBOOLE_1: 1;

        assume

         A5: C is everywhere_dense;

        then ( Int C) is everywhere_dense;

        then

         A6: D is everywhere_dense by Th61;

        assume B is everywhere_dense;

        then

         A7: (D /\ B) is everywhere_dense by A6, Th44;

        ( Int C) is dense by A5;

        then E is everywhere_dense by A7, A4, Th62;

        hence thesis by A3, Th38, XBOOLE_1: 17;

      end;

      thus thesis by A2, A3, Th38, Th61;

    end;

    theorem :: TOPS_3:65



     Th65: for A be Subset of X, B be Subset of X0 st A c= B holds B is boundary implies A is boundary by XBOOLE_1: 3, Th56;

    theorem :: TOPS_3:66



     Th66: for C,A be Subset of X, B be Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds A is boundary implies B is boundary by Th57;

    theorem :: TOPS_3:67

    for X0 be open non empty SubSpace of X holds for A be Subset of X, B be Subset of X0 st A = B holds A is boundary iff B is boundary

    proof

      let X0 be open non empty SubSpace of X;

      let A be Subset of X, B be Subset of X0;

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



       A1: C is open by TSEP_1:def 1;

      assume A = B;

      hence thesis by A1, Th65, Th66;

    end;

    theorem :: TOPS_3:68



     Th68: for A be Subset of X, B be Subset of X0 st A c= B holds B is nowhere_dense implies A is nowhere_dense

    proof

      let A be Subset of X, B be Subset of X0;

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

      reconsider G = (( Int ( Cl A)) /\ ( [#] X0)) as Subset of X0;

      assume

       A1: A c= B;

      then

      reconsider C = A as Subset of X0 by XBOOLE_1: 1;

      assume B is nowhere_dense;

      then C is nowhere_dense by A1, Th26;

      then

       A2: G is open & ( Int ( Cl C)) = {} by TOPS_2: 24;

      (( Int ( Cl A)) /\ ( [#] X0)) c= (( Cl A) /\ ( [#] X0)) by TOPS_1: 16, XBOOLE_1: 26;

      then

       A3: (( Int ( Cl A)) /\ ( [#] X0)) c= ( Cl C) by PRE_TOPC: 17;

      now

        assume ( Int ( Cl A)) <> {} ;

        then A meets ( Int ( Cl A)) by Th7;

        then

         A4: (A /\ ( Int ( Cl A))) <> {} ;

        C c= D;

        then (( Int ( Cl A)) /\ D) <> {} by A4, XBOOLE_1: 3, XBOOLE_1: 26;

        hence contradiction by A3, A2, TOPS_1: 24, XBOOLE_1: 3;

      end;

      hence thesis;

    end;



     Lm1: for C,A be Subset of X, B be Subset of X0 st C is open & C = the carrier of X0 & A = B holds A is nowhere_dense implies B is nowhere_dense

    proof

      let C,A be Subset of X, B be Subset of X0;

      assume

       A1: C is open;

      assume

       A2: C = the carrier of X0;

      assume A = B;

      then

       A3: ( Cl B) c= ( Cl A) by Th53;

      then

      reconsider D = ( Cl B) as Subset of X by XBOOLE_1: 1;

      assume A is nowhere_dense;

      then

       A4: ( Int ( Cl A)) = {} ;

      ( Int D) = ( Int ( Cl B)) by A1, A2, Th57;

      then ( Int ( Cl B)) = {} by A3, A4, TOPS_1: 19, XBOOLE_1: 3;

      hence thesis;

    end;

    theorem :: TOPS_3:69



     Th69: for C,A be Subset of X, B be Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds A is nowhere_dense implies B is nowhere_dense

    proof

      let C,A be Subset of X, B be Subset of X0;

      assume

       A1: C is open;

      assume

       A2: C c= the carrier of X0;

      assume that

       A3: A c= C and

       A4: A = B;

      assume

       A5: A is nowhere_dense;

       A6:

      now

        assume C <> {} ;

        then

        consider X1 be strict non empty SubSpace of X such that

         A7: C = the carrier of X1 by TSEP_1: 10;

        reconsider E = B as Subset of X1 by A3, A4, A7;

        E is nowhere_dense & X1 is SubSpace of X0 by A1, A2, A4, A5, A7, Lm1, TSEP_1: 4;

        hence thesis by Th68;

      end;

      now

        assume C = {} ;

        then B = ( {} X0) by A3, A4, XBOOLE_1: 3;

        hence thesis;

      end;

      hence thesis by A6;

    end;

    theorem :: TOPS_3:70

    for X0 be open non empty SubSpace of X holds for A be Subset of X, B be Subset of X0 st A = B holds A is nowhere_dense iff B is nowhere_dense

    proof

      let X0 be open non empty SubSpace of X;

      let A be Subset of X, B be Subset of X0;

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



       A1: C is open by TSEP_1:def 1;

      assume A = B;

      hence thesis by A1, Th68, Th69;

    end;

    begin

    theorem :: TOPS_3:71

    for X1,X2 be 1-sorted holds the carrier of X1 = the carrier of X2 implies for C1 be Subset of X1, C2 be Subset of X2 holds C1 = C2 iff (C1 ` ) = (C2 ` )

    proof

      let X1,X2 be 1-sorted;

      assume

       A1: the carrier of X1 = the carrier of X2;

      let C1 be Subset of X1, C2 be Subset of X2;

      thus C1 = C2 implies (C1 ` ) = (C2 ` ) by A1;

      thus (C1 ` ) = (C2 ` ) implies C1 = C2

      proof

        assume (C1 ` ) = (C2 ` );



        hence C1 = (( [#] X2) \ (C2 ` )) by A1, PRE_TOPC: 3

        .= C2 by PRE_TOPC: 3;

      end;

    end;

    reserve X1,X2 for TopStruct;

    theorem :: TOPS_3:72



     Th72: the carrier of X1 = the carrier of X2 & (for C1 be Subset of X1, C2 be Subset of X2 st C1 = C2 holds (C1 is open iff C2 is open)) implies the TopStruct of X1 = the TopStruct of X2

    proof

      assume

       A1: the carrier of X1 = the carrier of X2;

      assume

       A2: for C1 be Subset of X1, C2 be Subset of X2 st C1 = C2 holds (C1 is open iff C2 is open);

      now

        let D be object;

        assume

         A3: D in the topology of X2;

        then

        reconsider C2 = D as Subset of X2;

        reconsider C1 = C2 as Subset of X1 by A1;

        C2 is open by A3;

        then C1 is open by A2;

        hence D in the topology of X1;

      end;

      then

       A4: the topology of X2 c= the topology of X1 by TARSKI:def 3;

      now

        let D be object;

        assume

         A5: D in the topology of X1;

        then

        reconsider C1 = D as Subset of X1;

        reconsider C2 = C1 as Subset of X2 by A1;

        C1 is open by A5;

        then C2 is open by A2;

        hence D in the topology of X2;

      end;

      then the topology of X1 c= the topology of X2 by TARSKI:def 3;

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

    end;

    theorem :: TOPS_3:73



     Th73: the carrier of X1 = the carrier of X2 & (for C1 be Subset of X1, C2 be Subset of X2 st C1 = C2 holds (C1 is closed iff C2 is closed)) implies the TopStruct of X1 = the TopStruct of X2

    proof

      assume

       A1: the carrier of X1 = the carrier of X2;

      assume

       A2: for C1 be Subset of X1, C2 be Subset of X2 st C1 = C2 holds (C1 is closed iff C2 is closed);

      now

        let C1 be Subset of X1, C2 be Subset of X2;

        assume

         A3: C1 = C2;

        thus C1 is open implies C2 is open

        proof

          assume C1 is open;

          then (C1 ` ) is closed by TOPS_1: 4;

          then (C2 ` ) is closed by A1, A2, A3;

          hence thesis by TOPS_1: 4;

        end;

        thus C2 is open implies C1 is open

        proof

          assume C2 is open;

          then (C2 ` ) is closed by TOPS_1: 4;

          then (C1 ` ) is closed by A1, A2, A3;

          hence thesis by TOPS_1: 4;

        end;

      end;

      hence thesis by A1, Th72;

    end;

    reserve X1,X2 for TopSpace;

    theorem :: TOPS_3:74

    the carrier of X1 = the carrier of X2 & (for C1 be Subset of X1, C2 be Subset of X2 st C1 = C2 holds ( Int C1) = ( Int C2)) implies the TopStruct of X1 = the TopStruct of X2

    proof

      assume

       A1: the carrier of X1 = the carrier of X2;

      assume

       A2: for C1 be Subset of X1, C2 be Subset of X2 st C1 = C2 holds ( Int C1) = ( Int C2);

      now

        let C1 be Subset of X1, C2 be Subset of X2;

        assume

         A3: C1 = C2;

        thus C1 is open implies C2 is open

        proof

          assume C1 is open;

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

          then C2 = ( Int C2) by A2, A3;

          hence thesis;

        end;

        thus C2 is open implies C1 is open

        proof

          assume C2 is open;

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

          then C1 = ( Int C1) by A2, A3;

          hence thesis;

        end;

      end;

      hence thesis by A1, Th72;

    end;

    theorem :: TOPS_3:75

    the carrier of X1 = the carrier of X2 & (for C1 be Subset of X1, C2 be Subset of X2 st C1 = C2 holds ( Cl C1) = ( Cl C2)) implies the TopStruct of X1 = the TopStruct of X2

    proof

      assume

       A1: the carrier of X1 = the carrier of X2;

      assume

       A2: for C1 be Subset of X1, C2 be Subset of X2 st C1 = C2 holds ( Cl C1) = ( Cl C2);

      now

        let C1 be Subset of X1, C2 be Subset of X2;

        assume

         A3: C1 = C2;

        thus C1 is closed implies C2 is closed

        proof

          assume C1 is closed;

          then C1 = ( Cl C1) by PRE_TOPC: 22;

          then C2 = ( Cl C2) by A2, A3;

          hence thesis;

        end;

        thus C2 is closed implies C1 is closed

        proof

          assume C2 is closed;

          then C2 = ( Cl C2) by PRE_TOPC: 22;

          then C1 = ( Cl C1) by A2, A3;

          hence thesis;

        end;

      end;

      hence thesis by A1, Th73;

    end;

    reserve D1 for Subset of X1,

D2 for Subset of X2;

    theorem :: TOPS_3:76



     Th76: D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1 is open implies D2 is open);

    theorem :: TOPS_3:77



     Th77: D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies ( Int D1) = ( Int D2)

    proof

      assume

       A1: D1 = D2;



       A2: ( Int D1) c= D1 by TOPS_1: 16;

      then

      reconsider C2 = ( Int D1) as Subset of X2 by A1, XBOOLE_1: 1;

      assume

       A3: the TopStruct of X1 = the TopStruct of X2;

      then

       A4: C2 c= ( Int D2) by A1, A2, Th76, TOPS_1: 24;



       A5: ( Int D2) c= D2 by TOPS_1: 16;

      then

      reconsider C1 = ( Int D2) as Subset of X1 by A1, XBOOLE_1: 1;

      C1 c= ( Int D1) by A1, A3, A5, Th76, TOPS_1: 24;

      hence thesis by A4;

    end;

    theorem :: TOPS_3:78



     Th78: D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies ( Int D1) c= ( Int D2)

    proof

      assume

       A1: D1 c= D2;

      then

      reconsider C2 = D1 as Subset of X2 by XBOOLE_1: 1;

      assume the TopStruct of X1 = the TopStruct of X2;

      then ( Int D1) = ( Int C2) by Th77;

      hence thesis by A1, TOPS_1: 19;

    end;

    theorem :: TOPS_3:79



     Th79: D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1 is closed implies D2 is closed) by Th76;

    theorem :: TOPS_3:80



     Th80: D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies ( Cl D1) = ( Cl D2)

    proof

      assume

       A1: D1 = D2;

      assume

       A2: the TopStruct of X1 = the TopStruct of X2;

      then

      reconsider C2 = ( Cl D1) as Subset of X2;

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

      then

       A3: ( Cl D2) c= C2 by A1, A2, Th79, TOPS_1: 5;

      reconsider C1 = ( Cl D2) as Subset of X1 by A2;

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

      then ( Cl D1) c= C1 by A1, A2, Th79, TOPS_1: 5;

      hence thesis by A3;

    end;

    theorem :: TOPS_3:81



     Th81: D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies ( Cl D1) c= ( Cl D2)

    proof

      assume

       A1: D1 c= D2;

      assume

       A2: the TopStruct of X1 = the TopStruct of X2;

      then

      reconsider C2 = D1 as Subset of X2;

      ( Cl D1) = ( Cl C2) by A2, Th80;

      hence thesis by A1, PRE_TOPC: 19;

    end;

    theorem :: TOPS_3:82



     Th82: D2 c= D1 & the TopStruct of X1 = the TopStruct of X2 implies (D1 is boundary implies D2 is boundary)

    proof

      assume

       A1: D2 c= D1;

      then

      reconsider C1 = D2 as Subset of X1 by XBOOLE_1: 1;

      assume

       A2: the TopStruct of X1 = the TopStruct of X2;

      assume D1 is boundary;

      then C1 is boundary by A1, Th11;

      then

       A3: ( Int C1) = {} ;

      ( Int C1) = ( Int D2) by A2, Th77;

      hence thesis by A3;

    end;

    theorem :: TOPS_3:83



     Th83: D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1 is dense implies D2 is dense)

    proof

      assume

       A1: D1 c= D2;

      then

      reconsider C2 = D1 as Subset of X2 by XBOOLE_1: 1;

      assume

       A2: the TopStruct of X1 = the TopStruct of X2;

      assume D1 is dense;

      then

       A3: ( Cl D1) = the carrier of X1;

      ( Cl D1) = ( Cl C2) by A2, Th80;

      then C2 is dense by A2, A3;

      hence thesis by A1, TOPS_1: 44;

    end;

    theorem :: TOPS_3:84

    D2 c= D1 & the TopStruct of X1 = the TopStruct of X2 implies (D1 is nowhere_dense implies D2 is nowhere_dense)

    proof

      assume

       A1: D2 c= D1;

      assume

       A2: the TopStruct of X1 = the TopStruct of X2;

      assume D1 is nowhere_dense;

      then ( Cl D1) is boundary;

      then ( Cl D2) is boundary by A1, A2, Th81, Th82;

      hence thesis;

    end;

    reserve X1,X2 for non empty TopSpace;

    reserve D1 for Subset of X1,

D2 for Subset of X2;

    theorem :: TOPS_3:85

    D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1 is everywhere_dense implies D2 is everywhere_dense)

    proof

      assume

       A1: D1 c= D2;

      assume

       A2: the TopStruct of X1 = the TopStruct of X2;

      assume D1 is everywhere_dense;

      then ( Int D1) is dense;

      then ( Int D2) is dense by A1, A2, Th78, Th83;

      hence thesis;

    end;