TOPS_3

:: Remarks on Special Subsets of Topological Spaces
::  by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies PRE_TOPC, SUBSET_1, XBOOLE_0, STRUCT_0, TOPS_1, TARSKI, RCOMP_1,
      TOPS_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
      TSEP_1;
 constructors TOPS_1, BORSUK_1, TSEP_1;
 registrations PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1;
 requirements BOOLE, SUBSET;
 definitions XBOOLE_0;
 equalities XBOOLE_0, SUBSET_1, STRUCT_0;
 expansions PRE_TOPC, XBOOLE_0;
 theorems PRE_TOPC, TOPS_1, TOPS_2, TSEP_1, TDLAT_3, SUBSET_1, TARSKI,
      XBOOLE_0, XBOOLE_1;

begin

:: 1. Selected Properties of Subsets of a Topological Space.

reserve X for TopStruct,
  A for Subset of X;

theorem 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 Th2:
  (A = [#]X iff A` = {}X) & (A = the carrier of X iff A` = {})
by XBOOLE_1:37;

theorem Th3:
  for X being TopSpace, A,B being 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 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 Th5:
  for A being 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 Th6:
  for A being 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 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
  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

:: 2. Special Subsets of a Topological Space.

definition
  let X be TopStruct, A be Subset of X;
  redefine attr A is boundary means  :: redefines boundary (TOPS_1, definition)
  :Def1:
  Int A = {};
  compatibility by TOPS_1:48;
end;

theorem
  {}X is boundary;

reserve X for non empty TopSpace,
  A for Subset of X;

theorem 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 Th11:
  B is boundary & A c= B implies A is boundary
by TOPS_1:19,XBOOLE_1:3;

theorem
  A is boundary iff for C being Subset of X st A` c= C & C is closed
  holds C = the carrier of X
proof
  thus A is boundary implies for C being 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 being 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
  A is boundary iff for G being Subset of X st G <> {} & G is open holds
  ( A`) meets G
proof
  thus A is boundary implies for G being Subset of X st G <> {} & G is open
  holds ( A`) meets G
  by SUBSET_1:24,TOPS_1:50;
  assume
A1: for G being 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
  A is boundary iff for F being Subset of X holds F is closed implies
  Int F = Int(F \/ A)
proof
  thus A is boundary implies for F being 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 being Subset of X holds F is closed implies Int F = Int(F \/ A );
  then Int {}X = Int({}X \/ A);
  hence thesis;
end;

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

definition
  let X be TopStruct, A be Subset of X;
  redefine attr A is dense means  :: redefines dense (TOPS_1, definition)

  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
  [#]X is dense;

reserve X for non empty TopSpace,
  A, B for Subset of X;

theorem 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 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
  A is dense iff for C being Subset of X st A c= C & C is closed holds C
  = the carrier of X
by TOPS_1:5,PRE_TOPC:18;

theorem
  A is dense iff for G being Subset of X holds G is open implies Cl G =
  Cl(G /\ A)
proof
  thus A is dense implies for G being 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 being 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
  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;
  redefine attr A is nowhere_dense means  :: redefines nowhere_dense (TOPS_1, definition)

  Int(Cl A) = {};
  compatibility
  by Def1,TOPS_1:def 5;
end;

theorem
  {}X is nowhere_dense;

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

theorem
  A is nowhere_dense implies Cl A is nowhere_dense;

theorem
  A is nowhere_dense implies A is not dense
proof
  assume
A1: Int Cl A = {};
  assume A is dense;
  then Cl A = [#]X;
  hence contradiction by A1,TOPS_1:15;
end;

theorem 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 Th27:
  A is nowhere_dense iff ex C being Subset of X st A c= C & C is
  closed & C is boundary
proof
  thus A is nowhere_dense implies ex C being 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 being 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 Th28:
  A is nowhere_dense iff for G being Subset of X st G <> {} & G is
  open ex H being Subset of X st H c= G & H <> {} & H is open & A misses H
proof
  thus A is nowhere_dense implies for G being Subset of X st G <> {} & G is
  open ex H being 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 being 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 being Subset of X st G <> {} & G is open ex H being Subset of
  X st H c= G & H <> {} & H is open & A misses H;
  for G being Subset of X st G <> {} & G is open ex H being 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 being 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
  A is nowhere_dense implies A /\ B is nowhere_dense by Th26,XBOOLE_1:17;

theorem 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;
  attr A is everywhere_dense means

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

definition
  let X be TopStruct, A be Subset of X;
  redefine attr A is everywhere_dense means  :: redefines everywhere_dense (TOPS_3, definition)
  Cl(Int A) = the carrier of X;
  compatibility;
end;

theorem
  [#]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
  A is everywhere_dense implies Int A is everywhere_dense;

theorem 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
  A is everywhere_dense implies A <> {} by Th17,Th33;

theorem
  A is everywhere_dense iff Int A is dense;

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

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

theorem 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 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 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 Th41:
  A is everywhere_dense iff ex C being Subset of X st C c= A & C
  is open & C is dense
proof
  thus A is everywhere_dense implies ex C being 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 being Subset of X such that
A2: C c= A & C is open & C is dense;
  Int A is dense by A2,TOPS_1:24,44;
  hence thesis;
end;

theorem
  A is everywhere_dense iff for F being Subset of X st F <> the carrier
of X & F is closed ex H being 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 being Subset of X st F <> the
carrier of X & F is closed ex H being 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 being 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 being Subset of X st F <> the carrier of X & F is closed ex H
  being Subset of X st F c= H & H <> the carrier of X & H is closed & A \/ H =
  the carrier of X;
  for G being Subset of X st G <> {} & G is open ex H being 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 being 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
  A is everywhere_dense implies A \/ B is everywhere_dense by Th38,XBOOLE_1:7;

theorem 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 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
  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
  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
  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
  D is everywhere_dense implies ex C,B being 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 being 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,79;
end;

theorem
  D is everywhere_dense implies ex C,B being 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 being 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
  D is nowhere_dense implies ex C,B being 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 being 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
  D is nowhere_dense implies ex C,B being 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 being 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

:: 3. Properties of Subsets in Subspaces.

reserve Y0 for SubSpace of X;

theorem Th53:
  for A being Subset of X, B being 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 Th54:
  for C, A being Subset of X, B being 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,28;
  assume A = B;
  hence thesis by A3,PRE_TOPC:17;
end;

theorem
  for Y0 being closed non empty SubSpace of X for A being Subset of X, B
  being 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 Th56:
  for A being Subset of X, B being 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 Th57:
  for Y0 being non empty SubSpace of X, C, A being Subset of X, B
being 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,24;
  Int A c= Int B by A4,Th56;
  hence thesis by A6;
end;

theorem
  for Y0 being open non empty SubSpace of X for A being Subset of X, B
  being 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 Th59:
  for A being Subset of X, B being 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 Th60:
  for C, A being Subset of X, B being 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 Th61:
  for A being Subset of X, B being 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,44;
  hence thesis;
end;

theorem Th62:
  for C, A being Subset of X, B being 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,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
  for X0 being open non empty SubSpace of X for A,C being Subset of X, B
  being 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
  for C, A being Subset of X, B being 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 Th65:
  for A being Subset of X, B being Subset of X0 st A c= B holds B
  is boundary implies A is boundary
by XBOOLE_1:3,Th56;

theorem Th66:
  for C, A being Subset of X, B being 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
  for X0 being open non empty SubSpace of X for A being Subset of X, B
  being 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 Th68:
  for A being Subset of X, B being 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,26;
    hence contradiction by A3,A2,TOPS_1:24,XBOOLE_1:3;
  end;
  hence thesis;
end;

Lm1: for C, A being Subset of X, B being 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 Th69:
  for C, A being Subset of X, B being 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 being 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
  for X0 being open non empty SubSpace of X for A being Subset of X, B
  being 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

:: 4. Subsets in Topological Spaces with the same Topological Structures.

theorem
  for X1, X2 being 1-sorted holds the carrier of X1 = the carrier of X2
implies for C1 being Subset of X1, C2 being 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 Th72:
  the carrier of X1 = the carrier of X2 & (for C1 being Subset of
X1, C2 being 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 being Subset of X1, C2 being 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 Th73:
  the carrier of X1 = the carrier of X2 & (for C1 being Subset of
  X1, C2 being 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 being Subset of X1, C2 being 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
  the carrier of X1 = the carrier of X2 & (for C1 being Subset of X1, C2
  being 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 being Subset of X1, C2 being 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
  the carrier of X1 = the carrier of X2 & (for C1 being Subset of X1, C2
being 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 being Subset of X1, C2 being 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 Th76:
  D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1
  is open implies D2 is open);

theorem 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 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 Th79:
  D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1
  is closed implies D2 is closed)
by Th76;

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