:: On the Closure Operator and the Closure System of Many Sorted Sets
::  by Artur Korni{\l}owicz
::
:: Received February 7, 1996
:: Copyright (c) 1996-2019 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 PBOOLE, FUNCT_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ZFMISC_1,
      FUNCT_2, CARD_3, FINSET_1, COMPLEX1, SETFAM_1, FUNCT_4, MSSUBFAM,
      FUNCOP_1, RELAT_2, MSAFREE2, BINOP_1, YELLOW_6, STRUCT_0, MSUALG_1,
      PRE_TOPC, CLOSURE2, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FUNCT_4, PBOOLE, CARD_3,
      MSUALG_1, MBOOLEAN, MSSUBFAM;
 constructors SETFAM_1, FUNCT_4, MSSUBFAM, MSUALG_1, CARD_3, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
      FINSET_1, PBOOLE, MSUALG_1;
 requirements SUBSET, BOOLE;
 definitions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, CARD_3, TARSKI;
 equalities FUNCOP_1;
 expansions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, TARSKI;
 theorems FUNCOP_1, ENUMSET1, FUNCT_1, FUNCT_2, FUNCT_4, MBOOLEAN, PBOOLE,
      PZFMISC1, SETFAM_1, TARSKI, MSSUBFAM, ZFMISC_1, XBOOLE_0, XBOOLE_1,
      PARTFUN1, RELAT_1;
 schemes FRAENKEL, FUNCT_1, FUNCT_2, DOMAIN_1, XBOOLE_0;

begin  :: Preliminaries

reserve i, x, I for set,
  A, B, M for ManySortedSet of I,
  f, f1 for Function;

notation
  let I, A, B;
  synonym A in' B for A in B;
end;

notation
  let I, A, B;
  synonym A c=' B for A c= B;
end;

theorem
  for M being non empty set for X, Y being Element of M st X c= Y holds
  (id M).X c= (id M).Y;

theorem Th2:
  for I being non empty set for A being ManySortedSet of I for B
  being ManySortedSubset of A holds rng B c= union rng bool A
proof
  let I be non empty set, A be ManySortedSet of I, B be ManySortedSubset of A;
  let a be object;
  assume a in rng B;
  then consider i being object such that
A1: i in I and
A2: a = B.i by PBOOLE:138;
  i in dom bool A & bool (A.i) = (bool A).i by A1,MBOOLEAN:def 1,PARTFUN1:def 2
;
  then
A3: bool (A.i) in rng bool A by FUNCT_1:def 3;
  B c= A by PBOOLE:def 18;
  then B in bool A by MBOOLEAN:18;
  then B.i in (bool A).i by A1;
  then a in bool (A.i) by A1,A2,MBOOLEAN:def 1;
  hence thesis by A3,TARSKI:def 4;
end;

begin  :: Set of Many Sorted Subsets of a Many Sorted Set

definition
  let I, M;
  defpred f[object] means $1 is ManySortedSubset of M;
  func Bool M -> set means
  :Def1:
  for x being object holds x in it iff x is ManySortedSubset of M;
  existence
  proof
    per cases;
    suppose
A1:   I is non empty;
      consider X being set such that
A2:   for e being object holds e in X iff e in Funcs(I, union rng bool M)
      & f[e] from XBOOLE_0:sch 1;
      take X;
      let x be object;
        thus x in X implies x is ManySortedSubset of M by A2;
        assume
A3:     x is ManySortedSubset of M;
        now
          reconsider xx = x as ManySortedSubset of M by A3;
          dom xx = I & rng xx c= union rng bool M by A1,Th2,PARTFUN1:def 2;
          hence x in Funcs(I, union rng bool M) by FUNCT_2:def 2;
          thus f[ x ] by A3;
        end;
        hence thesis by A2;
    end;
    suppose
A4:   I is empty;
      take {EmptyMS {}};
      let x be object;
        thus x in {EmptyMS {}} implies x is ManySortedSubset of M
        proof
          reconsider M9 = M as ManySortedSet of {} by A4;
          assume
A5:       x in {EmptyMS {}};
          reconsider y = EmptyMS {} as ManySortedSubset of M9 by PBOOLE:def 18;
          y is ManySortedSubset of M by A4;
          hence thesis by A5,TARSKI:def 1;
        end;
        assume x is ManySortedSubset of M;
        then consider y being ManySortedSubset of M such that
A6:     y = x;
        y = EmptyMS {} by A4;
        hence thesis by A6,TARSKI:def 1;
      end;
  end;
  uniqueness
  proof
    thus for X1,X2 being set st
  (for x being object holds x in X1 iff f[ x ]) & (
for x being object holds x in X2 iff f[ x ])
holds X1 = X2 from XBOOLE_0:sch 3;
  end;
end;

registration
  let I, M;
  cluster Bool M -> non empty functional with_common_domain;
  coherence
  proof
    M is ManySortedSubset of M by PBOOLE:def 18;
    hence Bool M is non empty by Def1;
    thus Bool M is functional
    by Def1;
    let f, g be Function;
    assume that
A1: f in Bool M and
A2: g in Bool M;
A3: g is ManySortedSubset of M by A2,Def1;
    f is ManySortedSubset of M by A1,Def1;
    hence dom f = I by PARTFUN1:def 2
      .= dom g by A3,PARTFUN1:def 2;
  end;
end;

definition
  let I, M;
  mode SubsetFamily of M is Subset of Bool M;
end;

definition
  let I, M;
  redefine func Bool M -> SubsetFamily of M;
  coherence
  proof
    Bool M c= Bool M;
    hence thesis;
  end;
end;

registration
  let I, M;
  cluster non empty functional with_common_domain for SubsetFamily of M;
  existence
  proof
    take Bool M;
    thus thesis;
  end;
end;

registration
  let I, M;
  cluster empty finite for SubsetFamily of M;
  existence
  proof
    reconsider x = {} as SubsetFamily of M by XBOOLE_1:2;
    take x;
    thus thesis;
  end;
end;

reserve SF, SG for SubsetFamily of M;

definition
  let I, M;
  let S be non empty SubsetFamily of M;
  redefine mode Element of S -> ManySortedSubset of M;
  coherence
  proof
    let e be Element of S;
    thus thesis by Def1;
  end;
end;

theorem Th3: :: MSSUBFAM:34
  SF \/ SG is SubsetFamily of M;

theorem :: MSSUBFAM:35
  SF /\ SG is SubsetFamily of M;

theorem :: MSSUBFAM:36
  SF \ x is SubsetFamily of M;

theorem :: MSSUBFAM:37
  SF \+\ SG is SubsetFamily of M;

theorem Th7: :: MSSUBFAM:38
  A c= M implies {A} is SubsetFamily of M
proof
  assume A c= M;
  then A is ManySortedSubset of M by PBOOLE:def 18;
  then A in Bool M by Def1;
  hence thesis by ZFMISC_1:31;
end;

theorem Th8: :: MSSUBFAM:39
  A c= M & B c= M implies {A,B} is SubsetFamily of M
proof
  assume A c= M & B c= M;
  then {A} is SubsetFamily of M & {B} is SubsetFamily of M by Th7;
  then {A} \/ {B} is SubsetFamily of M by Th3;
  hence thesis by ENUMSET1:1;
end;

reserve E, T for Element of Bool M;

theorem Th9:
  E (/\) T in Bool M
proof
  E c= M & T c= M by PBOOLE:def 18;
  then E (/\) T c= M (/\) M by PBOOLE:21;
  then E (/\) T is ManySortedSubset of M by PBOOLE:def 18;
  hence thesis by Def1;
end;

theorem Th10:
  E (\/) T in Bool M
proof
  E c= M & T c= M by PBOOLE:def 18;
  then E (\/) T c= M (\/) M by PBOOLE:20;
  then E (\/) T is ManySortedSubset of M by PBOOLE:def 18;
  hence thesis by Def1;
end;

theorem
  E (\) A in Bool M
proof
  E c= M by PBOOLE:def 18;
  then E (\) A c= M by MBOOLEAN:15;
  then E (\) A is ManySortedSubset of M by PBOOLE:def 18;
  hence thesis by Def1;
end;

theorem
  E (\+\) T in Bool M
proof
  T c= M by PBOOLE:def 18;
  then
A1: T (\) E c= M by MBOOLEAN:15;
  E c= M by PBOOLE:def 18;
  then E (\) T c= M by MBOOLEAN:15;
  then E (\+\) T c= M by A1,PBOOLE:91;
  then E (\+\) T is ManySortedSubset of M by PBOOLE:def 18;
  hence thesis by Def1;
end;

begin  :: Many Sorted Operator corresponding
::  to the Operator on Many Sorted Subsets

definition
  let S be functional set;

  func |. S .| -> Function means
  :Def2:
  ex A being non empty functional set st
  A = S & dom it = meet the set of all  dom x where x is Element of A  &
  for i st i in dom it holds it.i = the set of all
 x.i where x is Element of A  if S <> {} otherwise it = {};
  existence
  proof
    thus S <> {} implies ex f being Function st ex A being non empty
functional set st A = S & dom f = meet the set of all
 dom x where x is Element of A  & for i st i in dom f holds f.i = the set of
all  x.i where x is Element of A

    proof
      assume S <> {};
      then consider A being non empty functional set such that
A1:   A = S;
      deffunc F(object)
  = the set of all  x.$1 where x is Element of A ;
      consider f being Function such that
A2:   dom f = meet the set of all  dom x where x is Element of A
 & for i being object st
i in meet the set of all  dom x where x is Element of A
      holds f.i = F (i) from FUNCT_1:sch 3;
      take f, A;
      thus thesis by A1,A2;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let f, g be Function;
    defpred P[Function] means ex A being non empty functional set st A = S &
dom $1 = meet the set of all  dom x where x is Element of A  & for i st
i in dom $1 holds $1.i = the set of all  x.i where x is Element of A ;
    thus S <> {} & P[f] & P[g] implies f = g
    proof
      assume that
      S <> {} and
A3:   P[f] and
A4:   P[g];
      consider A being non empty functional set such that
A5:   A = S and
A6:   dom f = meet the set of all dom x where x is Element of A and
A7:   for i st i in dom f holds f.i = the set of all
 x.i where x is Element of A  by A3;
      now
        let a be object;
        assume
A8:     a in meet the set of all  dom x where x is Element of A ;
        hence f.a = the set of all  x.a where x is Element of A  by A6
,A7
          .= g.a by A4,A5,A8;
      end;
      hence thesis by A4,A5,A6;
    end;
    thus thesis;
  end;
  consistency;
end;

theorem Th13:
  for SF being non empty SubsetFamily of M holds dom |.SF.| = I
proof
  let SF be non empty SubsetFamily of M;
  consider A being non empty functional set such that
A1: A = SF and
A2: dom |.SF.| = meet the set of all  dom x where x is Element of A  and
  for i st i in dom |.SF.| holds |.SF.|.i = the set of all
 x.i where x is Element of A
   by Def2;
  the set of all  dom x where x is Element of A  = {I}
  proof
    thus the set of all  dom x where x is Element of A  c= {I}
    proof
      let a be object;
      assume a in the set of all  dom x where x is Element of A ;
      then consider x being Element of A such that
A3:   a = dom x;
      x is Element of SF by A1;
      then a = I by A3,PARTFUN1:def 2;
      hence thesis by TARSKI:def 1;
    end;
    set x = the Element of A;
    let a be object;
    assume a in {I};
    then
A4: a = I by TARSKI:def 1;
    x is Element of SF by A1;
    then dom x = I by PARTFUN1:def 2;
    hence thesis by A4;
  end;
  hence thesis by A2,SETFAM_1:10;
end;

registration
  let S be empty functional set;
  cluster |. S .| -> empty;
  coherence by Def2;
end;

definition
  let I, M;
  let S be SubsetFamily of M;
  func |: S :| -> ManySortedSet of I equals
  :Def3:
  |. S .| if S <> {}
  otherwise EmptyMS I;
  coherence
  proof
    thus S <> {} implies |.S.| is ManySortedSet of I
    proof
      assume S <> {};
      then dom |.S.| = I by Th13;
      hence thesis by PARTFUN1:def 2,RELAT_1:def 18;
    end;
    thus thesis;
  end;
  consistency;
end;

registration
  let I, M;
  let S be empty SubsetFamily of M;
  cluster |: S :| -> empty-yielding;
  coherence
  proof
    |:S:| = EmptyMS I by Def3;
    hence thesis;
  end;
end;

theorem Th14:
  SF is non empty implies for i st i in I holds |:SF:|.i = { x.i
  where x is Element of Bool M : x in SF }
proof
A1: dom |:SF:| = I by PARTFUN1:def 2;
  assume
A2: SF is non empty;
  then consider A being non empty functional set such that
A3: A = SF and
  dom |.SF.| = meet the set of all  dom x where x is Element of A  and
A4: for i st i in dom |.SF.| holds |.SF.|.i = the set of all
 x.i where x is Element
  of A  by Def2;
  let i such that
A5: i in I;
  set K = { x.i where x is Element of Bool M : x in SF }, N = the set of all
 x.i where x is
  Element of A ;
A6: K = N
  proof
    thus K c= N
    proof
      let q be object;
      assume q in K;
      then ex x being Element of Bool M st q = x.i & x in SF;
      hence thesis by A3;
    end;
    let q be object;
    assume q in N;
    then consider x being Element of A such that
A7: q = x.i;
    x in SF by A3;
    hence thesis by A7;
  end;
  |:SF:| = |.SF.| by A2,Def3;
  hence thesis by A4,A5,A1,A6;
end;

registration
  let I, M;
  let SF be non empty SubsetFamily of M;
  cluster |: SF :| -> non-empty;
  coherence
  proof
    let i be object;
    assume i in I;
    then
A1: |:SF:|.i = { x.i where x is Element of Bool M : x in SF} by Th14;
    consider x being object such that
A2: x in SF by XBOOLE_0:def 1;
    reconsider x as Element of Bool M by A2;
    x.i in |:SF:|.i by A1,A2;
    hence thesis;
  end;
end;

theorem Th15:
  dom |.{f}.| = dom f
proof
  consider A being non empty functional set such that
A1: A = {f} and
A2: dom |.{f}.| = meet the set of all  dom x where x is Element of A  and
  for i st i in dom |.{f}.| holds |.{f}.|.i = the set of all
 x.i where x is Element of
A by Def2;
  set m = the set of all  dom x where x is Element of A ;
  m = {dom f}
  proof
    thus m c= {dom f}
    proof
      let q be object;
      assume q in m;
      then consider x being Element of A such that
A3:   q = dom x;
      x = f by A1,TARSKI:def 1;
      hence thesis by A3,TARSKI:def 1;
    end;
    let q be object;
    assume q in {dom f};
    then
A4: q = dom f by TARSKI:def 1;
    f is Element of A by A1,TARSKI:def 1;
    hence thesis by A4;
  end;
  hence thesis by A2,SETFAM_1:10;
end;

theorem
  dom |.{f,f1}.| = dom f /\ dom f1
proof
  consider A being non empty functional set such that
A1: A = {f,f1} and
A2: dom |.{f,f1}.| = meet the set of all  dom x where x is Element of A  and
  for i st i in dom |.{f,f1}.| holds |.{f,f1}.|.i = the set of all
 x.i where x is
  Element of A  by Def2;
  set m = the set of all  dom x where x is Element of A ;
  m = {dom f, dom f1}
  proof
    thus m c= {dom f, dom f1}
    proof
      let q be object;
      assume q in m;
      then consider x being Element of A such that
A3:   q = dom x;
      x = f or x = f1 by A1,TARSKI:def 2;
      hence thesis by A3,TARSKI:def 2;
    end;
    let q be object;
    assume q in {dom f, dom f1};
    then
A4: q = dom f or q = dom f1 by TARSKI:def 2;
    f is Element of A & f1 is Element of A by A1,TARSKI:def 2;
    hence thesis by A4;
  end;
  hence thesis by A2,SETFAM_1:11;
end;

theorem Th17:
  i in dom f implies |.{f}.|.i = {f.i}
proof
A1: f in {f} by TARSKI:def 1;
  consider A being non empty functional set such that
A2: A = {f} and
  dom |.{f}.| = meet the set of all  dom x where x is Element of A  and
A3: for i st i in dom |.{f}.| holds |.{f}.|.i = the set of all
 x.i where x is Element
  of A  by Def2;
  assume i in dom f;
  then i in dom |.{f}.| by Th15;
  then
A4: |.{f}.|.i = the set of all  x.i where x is Element of A  by A3;
  thus |.{f}.|.i c= { f.i }
  proof
    let q be object;
    assume q in |.{f}.|.i;
    then consider x being Element of A such that
A5: q = x.i by A4;
    x = f by A2,TARSKI:def 1;
    hence thesis by A5,TARSKI:def 1;
  end;
  let q be object;
  assume q in { f.i };
  then q = f.i by TARSKI:def 1;
  hence thesis by A2,A4,A1;
end;

theorem
  i in I & SF = {f} implies |:SF:|.i = {f.i}
proof
  assume that
A1: i in I and
A2: SF = {f};
A3: |:SF:| = |.SF.| by A2,Def3;
  dom |:SF:| = I by PARTFUN1:def 2;
  then i in dom f by A1,A2,A3,Th15;
  hence thesis by A2,A3,Th17;
end;

theorem Th19:
  i in dom |.{f,f1}.| implies |.{f,f1}.|.i = { f.i, f1.i }
proof
A1: f in {f,f1} & f1 in {f,f1} by TARSKI:def 2;
  consider A being non empty functional set such that
A2: A = {f,f1} and
  dom |.{f,f1}.| = meet the set of all  dom x where x is Element of A  and
A3: for i st i in dom |.{f,f1}.| holds |.{f,f1}.|.i = the set of all
 x.i where x is
  Element of A  by Def2;
  assume i in dom |.{f,f1}.|;
  then
A4: |.{f,f1}.|.i = the set of all  x.i where x is Element of A  by A3;
  thus |.{f,f1}.|.i c= { f.i, f1.i }
  proof
    let q be object;
    assume q in |.{f,f1}.|.i;
    then consider x being Element of A such that
A5: q = x.i by A4;
    per cases by A2,TARSKI:def 2;
    suppose
      x = f;
      hence thesis by A5,TARSKI:def 2;
    end;
    suppose
      x = f1;
      hence thesis by A5,TARSKI:def 2;
    end;
  end;
  let q be object;
  assume q in { f.i, f1.i };
  then q = f.i or q = f1.i by TARSKI:def 2;
  hence thesis by A2,A4,A1;
end;

theorem Th20:
  i in I & SF = {f,f1} implies |:SF:|.i = { f.i, f1.i }
proof
  assume that
A1: i in I and
A2: SF = {f,f1};
  dom |:SF:| = I & |:SF:| = |.SF.| by A2,Def3,PARTFUN1:def 2;
  hence thesis by A1,A2,Th19;
end;

definition
  let I, M, SF;
  redefine func |:SF:| -> MSSubsetFamily of M;
  coherence
  proof
    per cases;
    suppose
A1:   SF is non empty;
      |:SF:| is ManySortedSubset of bool M
      proof
        let i be object;
        assume
A2:     i in I;
        then
A3:     |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A1,Th14;
        thus |:SF:|.i c= (bool M).i
        proof
          let x be object;
          assume x in |:SF:|.i;
          then consider a being Element of Bool M such that
A4:       x = a.i and
          a in SF by A3;
          a c= M by PBOOLE:def 18;
          then a.i c= M.i by A2;
          then x in bool (M.i) by A4;
          hence thesis by A2,MBOOLEAN:def 1;
        end;
      end;
      hence thesis;
    end;
    suppose
      SF is empty;
      then |:SF:| = EmptyMS I;
      hence thesis by MSSUBFAM:31;
    end;
  end;
end;

theorem Th21:
  A in SF implies A in' |:SF:|
proof
  assume
A1: A in SF;
  let i be object;
  assume i in I;
  then |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A1,Th14;
  hence thesis by A1;
end;

theorem Th22:
  SF = {A,B} implies union |:SF:| = A (\/) B
proof
  assume
A1: SF = {A,B};
  now
    let i be object;
    assume
A2: i in I;
    hence (union |:SF:|).i = union (|:SF:|.i) by MBOOLEAN:def 2
      .= union { A.i, B.i } by A1,A2,Th20
      .= A.i \/ B.i by ZFMISC_1:75
      .= (A (\/) B).i by A2,PBOOLE:def 4;
  end;
  hence thesis;
end;

theorem Th23: :: SETFAM_1:12
  SF = {E,T} implies meet |:SF:| = E (/\) T
proof
  assume
A1: SF = { E,T };
  now
    reconsider sf1 = SF as non empty SubsetFamily of M by A1;
    let i be object such that
A2: i in I;
    ex Q be Subset-Family of (M.i) st Q = |:sf1:|.i & (meet |:sf1:|).i =
    Intersect Q by A2,MSSUBFAM:def 1;
    hence (meet |:SF:|).i = meet (|:sf1:|.i) by A2,SETFAM_1:def 9
      .= meet {E.i,T.i} by A1,A2,Th20
      .= E.i /\ T.i by SETFAM_1:11
      .= (E (/\) T).i by A2,PBOOLE:def 5;
  end;
  hence thesis;
end;

theorem Th24: :: MSSUBFAM:4
  for Z being ManySortedSubset of M st for Z1 being ManySortedSet
  of I st Z1 in SF holds Z c=' Z1 holds Z c=' meet |:SF:|
proof
  let Z be ManySortedSubset of M such that
A1: for Z1 be ManySortedSet of I st Z1 in SF holds Z c=' Z1;
  let i be object such that
A2: i in I;
  consider Q being Subset-Family of M.i such that
A3: Q = |:SF:|.i and
A4: (meet |:SF:|).i = Intersect Q by A2,MSSUBFAM:def 1;
A5: now
    let q be set such that
A6: q in Q;
    per cases;
    suppose
      SF is non empty;
      then |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A2,Th14
;
      then consider a being Element of Bool M such that
A7:   q = a.i and
A8:   a in SF by A3,A6;
      Z c=' a by A1,A8;
      hence Z.i c= q by A2,A7;
    end;
    suppose
      SF is empty;
      then |:SF:| = EmptyMS I;
      hence Z.i c= q by A3,A6;
    end;
  end;
  Z c= M by PBOOLE:def 18;
  then Z.i is Subset of M.i by A2;
  hence thesis by A4,A5,MSSUBFAM:4;
end;

theorem
  |: Bool M :| = bool M
proof
  now
    let i be object;
    assume
A1: i in I;
    then
A2: |:Bool M:|.i = { x.i where x is Element of Bool M : x in Bool M} by Th14;
    thus |: Bool M :|.i = (bool M).i
    proof
      thus |: Bool M :|.i c= (bool M).i
        by A1,PBOOLE:def 2,def 18;
      let a be object such that
A3:   a in (bool M).i;
      dom (EmptyMS I +* (i .--> a)) = I by A1,PZFMISC1:1;
      then reconsider X = EmptyMS I +* (i .--> a) as ManySortedSet of I by
PARTFUN1:def 2,RELAT_1:def 18;
A4:   dom (i .--> a) = {i};
      i in {i} by TARSKI:def 1;
      then
A5:   X.i = (i .--> a).i by A4,FUNCT_4:13
        .= a by FUNCOP_1:72;
      X is ManySortedSubset of M
      proof
        let s be object such that
A6:     s in I;
        per cases;
        suppose
A7:       s = i;
          then a in bool (M.s) by A3,A6,MBOOLEAN:def 1;
          hence thesis by A5,A7;
        end;
        suppose
          s <> i;
          then not s in dom (i .--> a) by TARSKI:def 1;
          then X.s = EmptyMS I.s by FUNCT_4:11
            .= {};
          hence thesis;
        end;
      end;
      then X is Element of Bool M by Def1;
      hence thesis by A2,A5;
    end;
  end;
  hence thesis;
end;

definition
  let I, M;
  let IT be SubsetFamily of M;
  attr IT is additive means
  for A, B st A in IT & B in IT holds A (\/) B in IT;
  attr IT is absolutely-additive means

  for F be SubsetFamily of M st F c= IT holds union |:F:| in IT;
  attr IT is multiplicative means
  for A, B st A in IT & B in IT holds A (/\) B in IT;
  attr IT is absolutely-multiplicative means
  :Def7:
  for F be SubsetFamily of M st F c= IT holds meet |:F:| in IT;
  attr IT is properly-upper-bound means
  :Def8:
  M in IT;
  attr IT is properly-lower-bound means

  EmptyMS I in IT;
end;

Lm1: Bool M is additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound
proof
  thus Bool M is additive
  by Th10;
  thus Bool M is absolutely-additive
  proof
    let F be SubsetFamily of M such that
    F c= Bool M;
    union |:F:| c= M by MSSUBFAM:40;
    then union |:F:| is ManySortedSubset of M by PBOOLE:def 18;
    hence thesis by Def1;
  end;
  thus Bool M is multiplicative
  by Th9;
  thus Bool M is absolutely-multiplicative
  by Def1;
  M is ManySortedSubset of M by PBOOLE:def 18;
  then M in Bool M by Def1;
  hence Bool M is properly-upper-bound;
  EmptyMS I c= M by PBOOLE:43;
  then EmptyMS I is ManySortedSubset of M by PBOOLE:def 18;
  hence EmptyMS I in Bool M by Def1;
end;

registration
  let I, M;
  cluster non empty functional with_common_domain additive absolutely-additive
    multiplicative absolutely-multiplicative properly-upper-bound
    properly-lower-bound for SubsetFamily of M;
  existence
  proof
    take Bool M;
    thus thesis by Lm1;
  end;
end;

definition
  let I, M;
  redefine func Bool M -> additive absolutely-additive multiplicative
  absolutely-multiplicative properly-upper-bound properly-lower-bound
  SubsetFamily of M;
  coherence by Lm1;
end;

registration
  let I, M;
  cluster absolutely-additive -> additive for SubsetFamily of M;
  coherence
  proof
    let SF be SubsetFamily of M such that
A1: SF is absolutely-additive;
    let A, B;
    assume that
A2: A in SF and
A3: B in SF;
    B is ManySortedSubset of M by A3,Def1;
    then
A4: B c= M by PBOOLE:def 18;
    A is ManySortedSubset of M by A2,Def1;
    then A c= M by PBOOLE:def 18;
    then reconsider ab = {A,B} as SubsetFamily of M by A4,Th8;
    {A} c= SF & {B} c= SF by A2,A3,ZFMISC_1:31;
    then {A} \/ {B} c= SF by XBOOLE_1:8;
    then {A,B} c= SF by ENUMSET1:1;
    then union |:ab:| in SF by A1;
    hence thesis by Th22;
  end;
end;

registration
  let I, M;
  cluster absolutely-multiplicative -> multiplicative for SubsetFamily of M;
  coherence
  proof
    let SF be SubsetFamily of M such that
A1: SF is absolutely-multiplicative;
    let A, B;
    assume that
A2: A in SF and
A3: B in SF;
    B is ManySortedSubset of M by A3,Def1;
    then
A4: B c= M by PBOOLE:def 18;
    A is ManySortedSubset of M by A2,Def1;
    then A c= M by PBOOLE:def 18;
    then reconsider ab = {A,B} as SubsetFamily of M by A4,Th8;
    {A} c= SF & {B} c= SF by A2,A3,ZFMISC_1:31;
    then {A} \/ {B} c= SF by XBOOLE_1:8;
    then {A,B} c= SF by ENUMSET1:1;
    then meet |:ab:| in SF by A1;
    hence thesis by A2,A3,Th23;
  end;
end;

registration
  let I, M;
  cluster absolutely-multiplicative -> properly-upper-bound for
SubsetFamily of M;
  coherence
  proof
    reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
    let SF be SubsetFamily of M such that
A1: SF is absolutely-multiplicative;
    |:a:| = EmptyMS I;
    then
A2: meet |:a:| = M by MSSUBFAM:41;
    a c= SF;
    hence M in SF by A1,A2;
  end;
end;

registration
  let I, M;
  cluster properly-upper-bound -> non empty for SubsetFamily of M;
  coherence;
end;

registration
  let I, M;
  cluster absolutely-additive -> properly-lower-bound for SubsetFamily of M;
  coherence
  proof
    reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
    let SF be SubsetFamily of M such that
A1: SF is absolutely-additive;
    |:a:| = EmptyMS I;
    then
A2: union |:a:| = EmptyMS I by MBOOLEAN:21;
    a c= SF;
    hence EmptyMS I in SF by A1,A2;
  end;
end;

registration
  let I, M;
  cluster properly-lower-bound -> non empty for SubsetFamily of M;
  coherence;
end;

begin  :: Properties of Closure Operators

definition
  let I, M;
  mode SetOp of M is Function of Bool M, Bool M;
end;

definition
  let I, M;
  let f be SetOp of M;
  let x be Element of Bool M;
  redefine func f.x -> Element of Bool M;
  coherence
  proof
    f.x in Bool M;
    hence thesis;
  end;
end;

definition
  let I, M;
  let IT be SetOp of M;

  attr IT is reflexive means
  :Def10:
  for x being Element of Bool M holds x c=' IT.x;
  attr IT is monotonic means
  :Def11:
  for x, y being Element of Bool M st x c=' y holds IT.x c=' IT.y;
  attr IT is idempotent means
  :Def12:
  for x being Element of Bool M holds IT.x = IT.(IT.x);
  attr IT is topological means

  for x, y being Element of Bool M holds IT.(x (\/) y) = (IT.x) (\/) (IT.y);
end;

registration
  let I, M;
  cluster reflexive monotonic idempotent topological for SetOp of M;
  existence
  proof
    reconsider f = id (Bool M) as SetOp of M;
    take f;
    thus f is reflexive;
    thus f is monotonic;
    thus f is idempotent;
    thus f is topological
    proof
      let X, Y be Element of Bool M;
      X c= M & Y c= M by PBOOLE:def 18;
      then X (\/) Y c= M by PBOOLE:16;
      then X (\/) Y is ManySortedSubset of M by PBOOLE:def 18;
      then X (\/) Y in Bool M by Def1;
      hence f.(X (\/) Y) = X (\/) Y by FUNCT_1:18
        .= f.X (\/) Y
        .= f.X (\/) f.Y;
    end;
  end;
end;

theorem :: CLOSURE:11
  id (Bool A) is reflexive SetOp of A
proof
  reconsider f = id (Bool A) as SetOp of A;
  f is reflexive;
  hence thesis;
end;

theorem :: CLOSURE:12
  id (Bool A) is monotonic SetOp of A
proof
  reconsider f = id (Bool A) as SetOp of A;
  f is monotonic;
  hence thesis;
end;

theorem :: CLOSURE:13
  id (Bool A) is idempotent SetOp of A
proof
  reconsider f = id (Bool A) as SetOp of A;
  f is idempotent;
  hence thesis;
end;

theorem :: CLOSURE:15
  id (Bool A) is topological SetOp of A
proof
  reconsider f = id (Bool A) as SetOp of A;
  f is topological
  proof
    let X, Y be Element of Bool A;
    X c= A & Y c= A by PBOOLE:def 18;
    then X (\/) Y c= A by PBOOLE:16;
    then X (\/) Y is ManySortedSubset of A by PBOOLE:def 18;
    then X (\/) Y in Bool A by Def1;
    hence f.(X (\/) Y) = X (\/) Y by FUNCT_1:18
      .= f.X (\/) Y
      .= f.X (\/) f.Y;
  end;
  hence thesis;
end;

reserve g, h for SetOp of M;

theorem :: CLOSURE:16
  E = M & g is reflexive implies E = g.E
proof
  assume
A1: E = M;
  assume g is reflexive;
  then
A2:   E c= g.E;
   g.E c= E by A1,PBOOLE:def 18;
 hence thesis by A2,PBOOLE:146;
end;

theorem :: CLOSURE:17
  (g is reflexive & for X being Element of Bool M holds g.X c= X)
  implies g is idempotent
proof
  assume that
A1: g is reflexive and
A2: for X being Element of Bool M holds g.X c= X;
  let X be Element of Bool M;
A3: g.X c= g.(g.X) by A1;
   g.(g.X) c= g.X by A2;
  hence thesis by A3,PBOOLE:146;
end;

theorem :: CLOSURE:18
  for A being Element of Bool M st A = E (/\) T holds g is monotonic
  implies g.A c= g.E (/\) g.T
proof
  let A be Element of Bool M such that
A1: A = E (/\) T;
  assume
A2: g is monotonic;
  E (/\) T c= T by PBOOLE:15;
  then
A3: g.A c= g.T by A1,A2;
  E (/\) T c= E by PBOOLE:15;
  then g.A c= g.E by A1,A2;
  hence thesis by A3,PBOOLE:17;
end;

registration
  let I, M;
  cluster topological -> monotonic for SetOp of M;
  coherence
  proof
    let g be SetOp of M such that
A1: g is topological;
    let X, Y be Element of Bool M such that
A2: X c= Y;
    g.X (\/) g.Y = g.(X (\/) Y) by A1
      .= g.Y by A2,PBOOLE:22;
    hence thesis by PBOOLE:26;
  end;
end;

theorem :: CLOSURE:19
  for A being Element of Bool M st A = E (\) T holds g is topological
  implies g.E (\) g.T c= g.A
proof
  let A be Element of Bool M such that
A1: A = E (\) T;
  assume
A2: g is topological;
  then g.E (\/) g.T = g.(E (\/) T)
    .= g.((E(\)T) (\/) T) by PBOOLE:67
    .= (g.A) (\/) (g.T) by A1,A2;
  then g.E c= g.A (\/) g.T by PBOOLE:14;
  then g.E (\) g.T c= (g.A (\/) g.T) (\) g.T by PBOOLE:53;
  then
A3: g.E (\) g.T c= g.A (\) g.T by PBOOLE:75;
  g.A (\) g.T c= g.A by PBOOLE:56;
  hence thesis by A3,PBOOLE:13;
end;

definition
  let I, M, h, g;
  redefine func g * h -> SetOp of M;
  coherence
  proof
    g * h is Function of Bool M, Bool M;
    hence thesis;
  end;
end;

theorem :: CLOSURE:21
  g is reflexive & h is reflexive implies g * h is reflexive
proof
  assume
A1: g is reflexive & h is reflexive;
  let X be Element of Bool M;
  X c= h.X & h.X c= g.(h.X) by A1;
  then dom h = Bool M & X c= g.(h.X) by FUNCT_2:def 1,PBOOLE:13;
  hence thesis by FUNCT_1:13;
end;

theorem :: CLOSURE:22
  g is monotonic & h is monotonic implies g * h is monotonic
proof
  assume that
A1: g is monotonic and
A2: h is monotonic;
A3: dom h = Bool M by FUNCT_2:def 1;
  let X, Y be Element of Bool M;
  assume X c= Y;
  then h.X c= h.Y by A2;
  then g.(h.X) c= g.(h.Y) by A1;
  then g.(h.X) c= (g*h).Y by A3,FUNCT_1:13;
  hence thesis by A3,FUNCT_1:13;
end;

theorem :: CLOSURE:23
  g is idempotent & h is idempotent & g*h = h*g implies g * h is idempotent
proof
  assume that
A1: g is idempotent and
A2: h is idempotent and
A3: g*h = h*g;
  let X be Element of Bool M;
A4: dom g = Bool M by FUNCT_2:def 1;
A5: dom h = Bool M by FUNCT_2:def 1;
  hence (g*h).X = g.(h.X) by FUNCT_1:13
    .= g.(h.(h.X)) by A2
    .= g.(g.(h.(h.X))) by A1
    .= g.((h*g).(h.X)) by A3,A5,FUNCT_1:13
    .= g.(h.(g.(h.X))) by A4,FUNCT_1:13
    .= g.(h.((g*h).X)) by A5,FUNCT_1:13
    .= (g*h).((g*h).X) by A5,FUNCT_1:13;
end;

theorem :: CLOSURE:25
  g is topological & h is topological implies g * h is topological
proof
  assume that
A1: g is topological and
A2: h is topological;
  let X, Y be Element of Bool M;
A3: dom h = Bool M by FUNCT_2:def 1;
  hence (g*h).(X (\/) Y) = g.(h.(X (\/) Y)) by Th10,FUNCT_1:13
    .= g.(h.X (\/) h.Y) by A2
    .= g.(h.X) (\/) g.(h.Y) by A1
    .= (g*h).X (\/) g.(h.Y) by A3,FUNCT_1:13
    .= (g*h).X (\/) (g*h).Y by A3,FUNCT_1:13;
end;

begin  :: On the Closure Operator and the Closure System

reserve S for 1-sorted;

definition
  let S;
  struct(many-sorted over S) ClosureStr over S (# Sorts -> ManySortedSet of
    the carrier of S, Family -> SubsetFamily of the Sorts #);
end;

reserve MS for many-sorted over S;

definition
  let S;
  let IT be ClosureStr over S;
  attr IT is additive means
  :Def14:
  the Family of IT is additive;
  attr IT is absolutely-additive means
  :Def15:
  the Family of IT is absolutely-additive;
  attr IT is multiplicative means
  :Def16:
  the Family of IT is multiplicative;
  attr IT is absolutely-multiplicative means
  :Def17:
  the Family of IT is absolutely-multiplicative;
  attr IT is properly-upper-bound means
  :Def18:
  the Family of IT is properly-upper-bound;
  attr IT is properly-lower-bound means
  :Def19:
  the Family of IT is properly-lower-bound;
end;

definition
  let S, MS;
  func Full MS -> ClosureStr over S equals
  ClosureStr (#the Sorts of MS, Bool the Sorts of MS#);
  correctness;
end;

registration
  let S, MS;
  cluster Full MS -> strict additive absolutely-additive multiplicative
    absolutely-multiplicative properly-upper-bound properly-lower-bound;
  coherence;
end;

registration
  let S;
  let MS be non-empty many-sorted over S;
  cluster Full MS -> non-empty;
  coherence;
end;

registration
  let S;
  cluster strict non-empty additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound for
ClosureStr
    over S;
  existence
  proof
    set a = the non-empty many-sorted over S;
    take Full a;
    thus thesis;
  end;
end;

registration
  let S;
  let CS be additive ClosureStr over S;
  cluster the Family of CS -> additive;
  coherence by Def14;
end;

registration
  let S;
  let CS be absolutely-additive ClosureStr over S;
  cluster the Family of CS -> absolutely-additive;
  coherence by Def15;
end;

registration
  let S;
  let CS be multiplicative ClosureStr over S;
  cluster the Family of CS -> multiplicative;
  coherence by Def16;
end;

registration
  let S;
  let CS be absolutely-multiplicative ClosureStr over S;
  cluster the Family of CS -> absolutely-multiplicative;
  coherence by Def17;
end;

registration
  let S;
  let CS be properly-upper-bound ClosureStr over S;
  cluster the Family of CS -> properly-upper-bound;
  coherence by Def18;
end;

registration
  let S;
  let CS be properly-lower-bound ClosureStr over S;
  cluster the Family of CS -> properly-lower-bound;
  coherence by Def19;
end;

registration
  let S;
  let M be non-empty ManySortedSet of the carrier of S;
  let F be SubsetFamily of M;
  cluster ClosureStr (#M, F#) -> non-empty;
  coherence;
end;

registration
  let S, MS;
  let F be additive SubsetFamily of the Sorts of MS;
  cluster ClosureStr (#the Sorts of MS, F#) -> additive;
  coherence;
end;

registration
  let S, MS;
  let F be absolutely-additive SubsetFamily of the Sorts of MS;
  cluster ClosureStr (#the Sorts of MS, F#) -> absolutely-additive;
  coherence;
end;

registration
  let S, MS;
  let F be multiplicative SubsetFamily of the Sorts of MS;
  cluster ClosureStr (#the Sorts of MS, F#) -> multiplicative;
  coherence;
end;

registration
  let S, MS;
  let F be absolutely-multiplicative SubsetFamily of the Sorts of MS;
  cluster ClosureStr (#the Sorts of MS, F#) -> absolutely-multiplicative;
  coherence;
end;

registration
  let S, MS;
  let F be properly-upper-bound SubsetFamily of the Sorts of MS;
  cluster ClosureStr (#the Sorts of MS, F#) -> properly-upper-bound;
  coherence;
end;

registration
  let S, MS;
  let F be properly-lower-bound SubsetFamily of the Sorts of MS;
  cluster ClosureStr (#the Sorts of MS, F#) -> properly-lower-bound;
  coherence;
end;

registration
  let S;
  cluster absolutely-additive -> additive for ClosureStr over S;
  coherence;
end;

registration
  let S;
  cluster absolutely-multiplicative -> multiplicative for ClosureStr over S;
  coherence;
end;

registration
  let S;
  cluster absolutely-multiplicative -> properly-upper-bound for
ClosureStr over S;
  coherence;
end;

registration
  let S;
  cluster absolutely-additive -> properly-lower-bound for ClosureStr over S;
  coherence;
end;

definition
  let S;
  mode ClosureSystem of S is absolutely-multiplicative ClosureStr over S;
end;

definition
  let I, M;
  mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M;
end;

definition
  let S;
  let A be ManySortedSet of the carrier of S;
  let g be ClosureOperator of A;
  func ClOp->ClSys g -> strict ClosureStr over S means
  :Def21:
  the Sorts of it = A &
  the Family of it = { x where x is Element of Bool A : g.x = x };
  existence
  proof
    defpred P[set] means g.$1 = $1;
    set SF = { x where x is Element of Bool A : P[ x ] };
    SF is Subset of Bool A from DOMAIN_1:sch 7;
    then reconsider D = SF as SubsetFamily of A;
    take ClosureStr (#A, D#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let S;
  let A be ManySortedSet of the carrier of S;
  let g be ClosureOperator of A;
  cluster ClOp->ClSys g -> absolutely-multiplicative;
  coherence
  proof
A1: the Sorts of ClOp->ClSys g = A by Def21;
    defpred P[set] means g.$1 = $1;
    set SF = { x where x is Element of Bool A : P[ x ] };
A2: SF = the Family of ClOp->ClSys g by Def21;
    SF is Subset of Bool A from DOMAIN_1:sch 7;
    then reconsider D = SF as SubsetFamily of A;
A3:    ClOp->ClSys g = ClosureStr (#A, D#) by A1,A2;
  D is absolutely-multiplicative
  proof
    let F be SubsetFamily of A such that
A4: F c= D;
    reconsider mf = meet |:F:| as Element of Bool A by Def1;
    now
      let Z1 be ManySortedSet of the carrier of S;
      assume
A5:   Z1 in F;
      then reconsider y1 = Z1 as Element of Bool A;
      Z1 in D by A4,A5;
      then
A6:   ex a being Element of Bool A st Z1 = a & g.a = a;
      mf c=' y1 by A5,Th21,MSSUBFAM:43;
      hence g.mf c=' Z1 by A6,Def11;
    end;
    then
A7: g.mf c=' mf by Th24;
    mf c=' g.mf by Def10;
    then g.mf = mf by A7,PBOOLE:146;
    hence thesis;
  end;
   hence ClOp->ClSys g is absolutely-multiplicative by A3;
  end;
end;

definition
  let S;
  let A be ClosureSystem of S;
  let C be ManySortedSubset of the Sorts of A;
  func Cl C -> Element of Bool the Sorts of A means
  :Def22:
  ex F being
SubsetFamily of the Sorts of A st it = meet |:F:| & F = { X where X is Element
  of Bool the Sorts of A : C c=' X & X in the Family of A };
  existence
  proof
    defpred P[Element of Bool the Sorts of A] means C c= $1 & $1 in the Family
    of A;
    { X where X is Element of Bool the Sorts of A : P[X] } is Subset of
    Bool the Sorts of A from DOMAIN_1:sch 7;
    then reconsider
    F = { X where X is Element of Bool the Sorts of A : C c= X & X
    in the Family of A } as SubsetFamily of the Sorts of A;
    reconsider IT = meet |:F:| as Element of Bool the Sorts of A by Def1;
    take IT,F;
    thus thesis;
  end;
  uniqueness;
end;

theorem Th38:
  for D being ClosureSystem of S for a being Element of Bool the
Sorts of D for f being SetOp of the Sorts of D st a in the Family of D & for x
  being Element of Bool the Sorts of D holds f.x = Cl x holds f.a = a
proof
  let D be ClosureSystem of S, a be Element of Bool the Sorts of D, f be SetOp
  of the Sorts of D such that
A1: a in the Family of D and
A2: for x being Element of Bool the Sorts of D holds f.x = Cl x;
  consider F being SubsetFamily of the Sorts of D such that
A3: Cl a = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : a c=' X & X in
  the Family of D } by Def22;
A5: f.a = meet |:F:| by A2,A3;
  a in F by A1,A4;
  then
A6: f.a c= a by A5,Th21,MSSUBFAM:43;
  for Z1 being ManySortedSet of the carrier of S st Z1 in F holds a c=' Z1
  proof
    let Z1 be ManySortedSet of the carrier of S;
    assume Z1 in F;
    then ex b being Element of Bool the Sorts of D st Z1 = b & a c=' b & b in
    the Family of D by A4;
    hence thesis;
  end;
  then a c= f.a by A5,Th24;
  hence thesis by A6,PBOOLE:146;
end;

theorem
  for D being ClosureSystem of S for a being Element of Bool the Sorts
  of D for f being SetOp of the Sorts of D st f.a = a & for x being Element of
  Bool the Sorts of D holds f.x = Cl x holds a in the Family of D
proof
  deffunc F(set) = $1;
  let D be ClosureSystem of S, a be Element of Bool the Sorts of D, f be SetOp
  of the Sorts of D such that
A1: f.a = a & for x being Element of Bool the Sorts of D holds f.x = Cl x;
  set F = the Family of D, M = the Sorts of D;
  defpred P[Element of Bool M] means a c=' $1;
  defpred R[Element of Bool M] means a c=' $1 & $1 in F;
  defpred S[Element of Bool M] means $1 in F & a c=' $1;
A2: { F(w) where w is Element of Bool M : F(w) in F & P[w] } c= F from
  FRAENKEL:sch 17;
A3: for q being Element of Bool M holds R[q] iff S[q];
A4: { F(s) where s is Element of Bool M : R[s] } = { F(b) where b is Element
  of Bool M : S[b] } from FRAENKEL:sch 3(A3);
  consider SF being SubsetFamily of M such that
A5: Cl a = meet |:SF:| and
A6: SF = { X where X is Element of Bool M : a c= X & X in F } by Def22;
  a = meet |:SF:| by A1,A5;
  hence thesis by A6,A2,A4,Def7;
end;

theorem Th40:
  for D being ClosureSystem of S for f being SetOp of the Sorts of
  D st for x being Element of Bool the Sorts of D holds f.x = Cl x holds f is
  reflexive monotonic idempotent
proof
  let D be ClosureSystem of S, f be SetOp of the Sorts of D such that
A1: for x being Element of Bool the Sorts of D holds f.x = Cl x;
  set M = the Sorts of D;
A2: f is reflexive
  proof
    let x be Element of Bool M;
    consider F being SubsetFamily of M such that
A3: Cl x = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : x c=' X & X in
    the Family of D } by Def22;
A5: for Z1 being ManySortedSet of the carrier of S st Z1 in F holds x c=' Z1
    proof
      let Z1 be ManySortedSet of the carrier of S;
      assume Z1 in F;
      then
      ex a being Element of Bool M st Z1 = a & x c=' a & a in the Family of
      D by A4;
      hence thesis;
    end;
    f.x = meet |:F:| by A1,A3;
    hence thesis by A5,Th24;
  end;
A6: f is monotonic
  proof
    let x, y be Element of Bool M such that
A7: x c=' y;
    consider Fy being SubsetFamily of M such that
A8: Cl y = meet |:Fy:| and
A9: Fy = { X where X is Element of Bool the Sorts of D : y c=' X & X
    in the Family of D } by Def22;
    consider Fx being SubsetFamily of M such that
A10: Cl x = meet |:Fx:| and
A11: Fx = { X where X is Element of Bool the Sorts of D : x c=' X & X
    in the Family of D } by Def22;
    |:Fy:| c=' |:Fx:|
    proof
      let i be object such that
A12:  i in the carrier of S;
      thus |:Fy:|.i c= |:Fx:|.i
      proof
        let q be object such that
A13:    q in |:Fy:|.i;
        per cases;
        suppose
          Fy is empty;
          then reconsider Fy9 = Fy as empty SubsetFamily of M;
          |:Fy9:|.i is empty;
          hence thesis by A13;
        end;
        suppose
          Fy is non empty;
          then |:Fy:|.i = { e.i where e is Element of Bool M : e in Fy } by A12
,Th14;
          then consider w being Element of Bool M such that
A14:      q = w.i and
A15:      w in Fy by A13;
A16:      ex r being Element of Bool M st r = w & y c=' r & r in the
          Family of D by A9,A15;
          then x c=' w by A7,PBOOLE:13;
          then
A17:      w in Fx by A11,A16;
          then |:Fx:|.i = { e.i where e is Element of Bool M : e in Fx } by A12
,Th14;
          hence thesis by A14,A17;
        end;
      end;
    end;
    then meet |:Fx:| c=' meet |:Fy:| by MSSUBFAM:46;
    then meet |:Fx:| c=' f.y by A1,A8;
    hence thesis by A1,A10;
  end;
  f is idempotent
  proof
    let x be Element of Bool M;
    consider F being SubsetFamily of M such that
A18: Cl x = meet |:F:| and
A19: F = { X where X is Element of Bool the Sorts of D : x c=' X & X
    in the Family of D } by Def22;
    F c= the Family of D
    proof
      let k be object;
      assume k in F;
      then
      ex q being Element of Bool M st k = q & x c=' q & q in the Family of
      D by A19;
      hence thesis;
    end;
    then
A20: meet |:F:| in the Family of D by Def7;
    thus f.x = meet |:F:| by A1,A18
      .= f.(meet |:F:|) by A1,A20,Th38
      .= f.(f.x) by A1,A18;
  end;
  hence thesis by A2,A6;
end;

definition
  let S;
  let D be ClosureSystem of S;
  func ClSys->ClOp D -> ClosureOperator of the Sorts of D means
  :Def23:
  for x being Element of Bool the Sorts of D holds it.x = Cl x;
  existence
  proof
    set M = the Sorts of D;
    deffunc F(Element of Bool M) = Cl $1;
    consider f being Function of Bool M, Bool M such that
A1: for x being Element of Bool M holds f.x = F(x) from FUNCT_2:sch 4;
    reconsider f as SetOp of M;
    reconsider f as ClosureOperator of M by A1,Th40;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f, g be ClosureOperator of the Sorts of D such that
A2: for x being Element of Bool the Sorts of D holds f.x = Cl x and
A3: for x being Element of Bool the Sorts of D holds g.x = Cl x;
    now
      set X = Bool the Sorts of D;
      thus X = dom f by FUNCT_2:def 1;
      thus X = dom g by FUNCT_2:def 1;
      let x be object;
      assume x in X;
      then reconsider x1 = x as Element of Bool the Sorts of D;
      thus f.x = Cl x1 by A2
        .= g.x by A3;
    end;
    hence f = g;
  end;
end;

theorem
  for A being ManySortedSet of the carrier of S for f being
  ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
proof
  let A be ManySortedSet of the carrier of S, f be ClosureOperator of A;
  set D = ClOp->ClSys f, M = the Sorts of D, f1 = ClSys->ClOp D;
A1: A = M by Def21;
  then reconsider ff = f as reflexive idempotent monotonic SetOp of M;
  for x being object st x in Bool A holds f1.x = ff.x
  proof
    let x be object;
    assume x in Bool A;
    then reconsider x1 = x as Element of Bool M by Def21;
    consider F being SubsetFamily of M such that
A2: Cl x1 = meet |:F:| and
A3: F = { X where X is Element of Bool M : x1 c=' X & X in the Family
    of D } by Def22;
A4: now
A5:   x1 c=' ff.x1 by Def10;
      x1 c=' M & M in the Family of D by Def8,PBOOLE:def 18;
      then M in F by A3;
      then reconsider F9 = F as non empty SubsetFamily of M;
      let i be object;
      assume
A6:   i in the carrier of S;
      then consider Q be Subset-Family of (M.i) such that
A7:   Q = |:F:|.i and
A8:   (meet |:F:|).i = Intersect Q by MSSUBFAM:def 1;
A9:   Q = { q.i where q is Element of Bool M : q in F9 } by A6,A7,Th14;
A10:  the Family of D = { q where q is Element of Bool M : ff.q = q } by A1
,Def21;
A11:  now
        let z be set;
        assume z in Q;
        then consider q being Element of Bool M such that
A12:    z = q.i and
A13:    q in F9 by A9;
        consider X being Element of Bool M such that
A14:    q = X and
A15:    x1 c=' X & X in the Family of D by A3,A13;
        (ex t being Element of Bool M st X = t & ff.t = t )& ff.x1 c=' ff
        .X by A10,A15,Def11;
        hence ff.x1.i c= z by A6,A12,A14;
      end;
      ff.(ff.x1) = ff.x1 by Def12;
      then ff.x1 in the Family of D by A10;
      then ff.x1 in F9 by A3,A5;
      then ff.x1.i in Q by A9;
      then
A16:  (meet |:F:|).i c= ff.x1.i by A8,MSSUBFAM:2;
      Q = |:F9:|.i by A7;
      then ff.x1.i c= (meet |:F:|).i by A6,A8,A11,MSSUBFAM:5;
      hence (meet |:F:|).i = ff.x1.i by A16;
    end;
    thus f1.x = Cl x1 by Def23
      .= ff.x by A2,A4,PBOOLE:3;
  end;
  hence thesis by A1,FUNCT_2:12;
end;

deffunc F(set) = $1;

theorem
  for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = the
  ClosureStr of D
proof
  let D be ClosureSystem of S;
  set M = the Sorts of D, F = the Family of D, d = the Family of ClOp->ClSys (
  ClSys->ClOp D), f = ClSys->ClOp D;
A1: d = { x where x is Element of Bool M : f.x = x } by Def21;
  F = d
  proof
    thus F c= d
    proof
      let q be object;
      assume
A2:   q in F;
      then reconsider q1 = q as Element of Bool M;
      consider SF being SubsetFamily of M such that
A3:   Cl q1 = meet |:SF:| and
A4:   SF = { X where X is Element of Bool M : q1 c= X & X in F } by Def22;
      q1 c=' M & M in F by Def8,PBOOLE:def 18;
      then M in SF by A4;
      then reconsider SF9 = SF as non empty SubsetFamily of M;
      now
        let i be object;
        assume
A5:     i in the carrier of S;
        then consider Q be Subset-Family of (M.i) such that
A6:     Q = |:SF9:|.i and
A7:     (meet |:SF9:|).i = Intersect Q by MSSUBFAM:def 1;
A8:     Q = { x.i where x is Element of Bool M : x in SF9 } by A5,A6,Th14;
        q1 in SF9 by A2,A4;
        then
A9:     q1.i in Q by A8;
        then
A10:    Intersect Q c= q1.i by MSSUBFAM:2;
        now
          let z be set;
          assume z in Q;
          then consider x being Element of Bool M such that
A11:      z = x.i and
A12:      x in SF9 by A8;
          ex xx being Element of Bool M st xx = x & q1 c=' xx & xx in F by A4
,A12;
          hence q1.i c= z by A5,A11;
        end;
        then q1.i c= Intersect Q by A9,MSSUBFAM:5;
        then Intersect Q = q1.i by A10;
        hence f.q1.i = q1.i by A3,A7,Def23;
      end;
      then f.q1 = q1;
      hence thesis by A1;
    end;
    let q be object;
    assume q in d;
    then consider x being Element of Bool M such that
A13: q = x & f.x = x by A1;
    defpred S[Element of Bool M] means $1 in F & x c=' $1;
    defpred R[Element of Bool M] means x c=' $1 & $1 in F;
    defpred P[Element of Bool M] means x c=' $1;
A14: { F(w) where w is Element of Bool M : F(w) in F & P[w] } c= F from
    FRAENKEL:sch 17;
A15: for a being Element of Bool M holds R[a] iff S[a];
A16: { F(a) where a is Element of Bool M : R[a] } = { F(b) where b is
    Element of Bool M : S[b] } from FRAENKEL:sch 3(A15);
    consider SF being SubsetFamily of M such that
A17: Cl x = meet |:SF:| and
A18: SF = { X where X is Element of Bool M : x c=' X & X in F } by Def22;
    meet |:SF:| = q by A13,A17,Def23;
    hence thesis by A18,A14,A16,Def7;
  end;
  hence thesis by Def21;
end;