TDLAT_1

:: The Lattice of Domains of a Topological Space
::  by Toshihiko Watanabe
::
:: Received June 12, 1992
:: Copyright (c) 1992-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, TARSKI, TOPS_1, RCOMP_1, SETFAM_1,
      ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, MCART_1, LATTICES, EQREL_1,
      REALSET1, NAT_LAT, TDLAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, STRUCT_0, PRE_TOPC,
      LATTICES, BINOP_1, TOPS_1, FUNCT_1, DOMAIN_1, FUNCT_2, NAT_LAT;
 constructors PARTFUN1, BINOP_1, REALSET1, TOPS_1, NAT_LAT;
 registrations SUBSET_1, REALSET1, LATTICES, TOPS_1, RELAT_1, PRE_TOPC;
 requirements BOOLE, SUBSET;
 definitions TARSKI, LATTICES, NAT_LAT;
 equalities LATTICES, XBOOLE_0, BINOP_1, REALSET1, SUBSET_1, STRUCT_0;
 expansions TARSKI, XBOOLE_0;
 theorems TOPS_1, PRE_TOPC, LATTICE2, BINOP_1, FUNCT_2, SUBSET_1, MCART_1,
      FUNCT_1, XBOOLE_1, XTUPLE_0, ZFMISC_1;
 schemes FUNCT_2, BINOP_2;

begin

:: 1. Preliminary Theorems on Subsets of Topological Spaces.

reserve T for 1-sorted;

theorem Th1:
  for A,B being 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 Th2:
  for A,B being Subset of T holds A misses B iff B c= A` by SUBSET_1:23;

reserve T for TopSpace;

theorem Th3:
  for A being 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 Th4:
  for A being 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 Th5:
  for A being 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 Th6:
  for A,B being 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 Th7:
  for A,B being 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 Th8:
  for A being 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 Th9:
  for A being 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 Th10:
  for A,B being 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,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
  for A,C being 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 Th12:
  for A,B being 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,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
  for A,C being 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

:: 2. Properties of Domains_of of Topological Spaces.

theorem 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 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 Th16:
  for A being 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 Th17:
  for A,B being 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 Th18:
  {} T is closed_condensed
proof
  Cl Int {} T = {} T by PRE_TOPC:22;
  hence thesis by TOPS_1:def 7;
end;

theorem 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 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 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 Th22:
  for A being 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 Th23:
  for A being 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 Th24:
  for A being 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 Th25:
  for A being 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
  for A being Subset of T st A is condensed holds Cl A` is
  closed_condensed by Th16,Th24;

theorem
  for A being Subset of T st A is condensed holds Int A` is
  open_condensed by Th16,Th25;

theorem Th28:
  for A,B,C being 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 Th29:
  for A,B,C being 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

:: 3. The Lattice of Domains.

definition
  let T be TopStruct;
  func Domains_of T -> Subset-Family of T equals
  { A where A is Subset of T :
  A is condensed };
  coherence
  proof
    set B = { A where A is 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 being 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 is Subset of T : A is condensed };
    hence thesis;
  end;
end;

definition
  let T be TopSpace;
  func Domains_Union T -> BinOp of Domains_of T means
  :Def2:
  for A,B being
  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 being 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 being Element of D ex b being 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 is Subset of T : H is condensed };
      then
A2:   ex H being Subset of T st H = F & H is condensed;
      G in { E where E is Subset of T : E is condensed };
      then ex E being 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 is 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 being Function of D, Domains_of T such that
A5: for a being 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 being BinOp of Domains_of T st (for a,b being Element of
Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being 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;
  func Domains_Meet T -> BinOp of Domains_of T means
  :Def3:
  for A,B being
  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 being 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 being Element of D ex b being 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 is Subset of T : H is condensed };
      then
A2:   ex H being Subset of T st H = F & H is condensed;
      G in { E where E is Subset of T : E is condensed };
      then ex E being 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 is 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 being Function of D, Domains_of T such that
A5: for a being 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 being BinOp of Domains_of T st (for a,b being Element of
Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being 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 Th30:
  for T being 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 is Subset of T : D is condensed };
    then ex D being 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
,12
      .= Int(Cl(B)) \/ B by A3,A5,XBOOLE_1: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 is Subset of T : D is condensed };
    then ex D being 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
,28
      .= Cl(Int(A)) /\ A by A10,A12,XBOOLE_1: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 is 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 is 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 is 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 is Subset of T : D is condensed};
    then ex D being Subset of T st D = B & D is condensed;
    then B` is condensed by Th16;
    then B` in { D where D is Subset of T : D is condensed};
    then reconsider a = B` as Element of L;
    take a;
A16: for v being 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 is Subset of T : D is condensed};
      then ex D being 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 is Subset of T : D is condensed};
    then reconsider c = {} T as Element of L;
A18: for v being 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 is Subset of T : D is condensed};
      then ex D being 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;
  func Domains_Lattice T -> C_Lattice equals
  LattStr(#Domains_of T,
    Domains_Union T,Domains_Meet T#);
  coherence by Th30;
end;

begin

:: 4. The Lattice of Closed Domains.

definition
  let T be TopStruct;
  func Closed_Domains_of T -> Subset-Family of T equals
  { A where A is Subset
  of T : A is closed_condensed };
  coherence
  proof
    set B = { A where A is 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 being 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 is Subset of T : A is closed_condensed };
    hence thesis;
  end;
end;

theorem Th31:
  for T being 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 is Subset of T : A is closed_condensed }; then
    consider A1 being 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 is Subset of T : A is condensed } by A1;
    hence thesis;
  end;

definition
  let T be TopSpace;
  func Closed_Domains_Union T -> BinOp of Closed_Domains_of T means
  :Def6:
  for A,B being Element of Closed_Domains_of T holds it.(A,B) = A \/ B;
  existence
  proof
    defpred X[set,set] means for A,B being 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 being Element of D ex b being 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 is Subset of T : E is closed_condensed };
      then consider E being Subset of T such that
A2:   E = G and
A3:   E is closed_condensed;
      F in { H where H is Subset of T : H is closed_condensed };
      then consider H being 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 is 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 being Function of D, Closed_Domains_of T such that
A7: for a being 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 being BinOp of Closed_Domains_of T st (for a,b being
    Element of Closed_Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being
    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 Th32:
  for A,B being 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 is 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 is Subset of T : E is closed_condensed };
  then consider E being Subset of T such that
A2: E = B and
A3: E is closed_condensed;
  consider D being 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;
  func Closed_Domains_Meet T -> BinOp of Closed_Domains_of T means
  :Def7:
  for
  A,B being Element of Closed_Domains_of T holds it.(A,B) = Cl(Int(A /\ B));
  existence
  proof
    defpred X[set,set] means for A,B being 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 being Element of D ex b being 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 is 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 being Function of D, Closed_Domains_of T such that
A3: for a being 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 being BinOp of Closed_Domains_of T st (for a,b being
    Element of Closed_Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being
    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 Th33:
  for A,B being 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 is Subset of T : D is closed_condensed };
  then consider D being 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 is Subset of T : E is closed_condensed };
  then consider E being 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 Th34:
  for T being 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 is Subset of T : D is closed_condensed };
    then ex D being 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,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 is Subset of T : D is closed_condensed };
    then
A7: ex D being 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 is Subset of T : D is closed_condensed };
    then
A11: ex D being Subset of T st D = A & D is closed_condensed;
    B in { E where E is Subset of T : E is closed_condensed };
    then
A12: ex E being Subset of T st E = B & E is closed_condensed;
    C in { F where F is Subset of T : F is closed_condensed };
    then
A13: ex F being 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 is 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 is Subset of T : D is closed_condensed };
    then consider D being 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 is Subset of T : E is closed_condensed };
    then consider E being 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 is 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 is Subset of T : D is closed_condensed};
    then consider D being 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 is 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 being 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 is Subset of T : K is closed_condensed};
      then
A30:  ex D being 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 is Subset of T : K is closed_condensed};
    then reconsider c = {} T as Element of L;
A31: for v being 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 is 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;
  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

:: 5. The Lattice of Open Domains.

definition
  let T be TopStruct;
  func Open_Domains_of T -> Subset-Family of T equals
  { A where A is Subset of
T: A is open_condensed };
  coherence
  proof
    set B = { A where A is 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 being 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 is Subset of T : A is open_condensed };
    hence thesis;
  end;
end;

theorem Th35:
  for T being 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 is Subset of T : A is open_condensed }; then
    consider A1 being 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 is Subset of T : A is condensed } by A1;
    hence thesis;
  end;

definition
  let T be TopSpace;
  func Open_Domains_Union T -> BinOp of Open_Domains_of T means
  :Def10:
  for A, B being Element of Open_Domains_of T holds it.(A,B) = Int(Cl(A \/ B));
  existence
  proof
    defpred X[set,set] means for A,B being 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 being Element of D ex b being 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 is 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 being Function of D, Open_Domains_of T such that
A3: for a being 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 being BinOp of Open_Domains_of T st (for a,b being Element
    of Open_Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being 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 Th36:
  for A,B being 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 is Subset of T : D is open_condensed };
  then consider D being 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 is Subset of T : E is open_condensed };
  then consider E being 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;
  func Open_Domains_Meet T -> BinOp of Open_Domains_of T means
  :Def11:
  for A,B being Element of Open_Domains_of T holds it.(A,B) = A /\ B;
  existence
  proof
    defpred X[set,set] means for A,B being 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 being Element of D ex b being 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 is Subset of T : E is open_condensed };
      then consider E being Subset of T such that
A2:   E = G and
A3:   E is open_condensed;
      F in { H where H is Subset of T : H is open_condensed };
      then consider H being 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 is 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 being Function of D, Open_Domains_of T such that
A7: for a being 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 being BinOp of Open_Domains_of T st (for a,b being Element
    of Open_Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being 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 Th37:
  for A,B being 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 is 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 is Subset of T : E is open_condensed };
  then consider E being Subset of T such that
A2: E = B and
A3: E is open_condensed;
  consider D being 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 Th38:
  for T being 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 is Subset of T : D is open_condensed };
    then
A3: ex D being 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 is Subset of T : D is open_condensed };
    then ex D being 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,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 is Subset of T : D is open_condensed };
    then
A11: ex D being Subset of T st D = A & D is open_condensed;
    B in { E where E is Subset of T : E is open_condensed };
    then
A12: ex E being Subset of T st E = B & E is open_condensed;
    C in { F where F is Subset of T : F is open_condensed };
    then
A13: ex F being 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 is 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 is Subset of T : D is open_condensed };
    then consider D being 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 is Subset of T : F is open_condensed };
    then consider F being Subset of T such that
A22: F = C and
    F is open_condensed;
    B in { E where E is Subset of T : E is open_condensed };
    then consider E being 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 is 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 is Subset of T : D is open_condensed};
    then consider D being 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 is 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 being 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 is Subset of T : K is open_condensed};
    then reconsider c = {} T as Element of L;
A31: for v being 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 is Subset of T : K is open_condensed};
      then
A32:  ex D being 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 is 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;
  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

:: 6. Connections between Lattices of Domains.

theorem 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 being Element of Closed_Domains_of T, B being 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 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 being Element of Closed_Domains_of T, B being 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
  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 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 being Element of Open_Domains_of T, B being 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 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 being Element of Open_Domains_of T, B being 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
  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;