:: On the Closure Operator and the Closure System of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received February 7, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

notation
let I be set ;
let A, B be ManySortedSet of I;
synonym A in' B for A in B;
end;

notation
let I be set ;
let A, B be ManySortedSet of I;
synonym A c=' B for A c= B;
end;

theorem :: CLOSURE2:1
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
proofend;

theorem Th2: :: CLOSURE2:2
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))
proofend;

begin

definition
let I be set ;
let M be ManySortedSet of I;
defpred S1[ set ] means $1 is ManySortedSubset of M;
func Bool M ->  set  means :Def1: :: CLOSURE2:def 1
 for x being set holds
( x in it iff x is ManySortedSubset of M );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedSubset of M )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is ManySortedSubset of M ) ) & ( for x being set holds
( x in b2 iff x is ManySortedSubset of M ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Bool CLOSURE2:def_1_:_
 for I being set
for M being ManySortedSet of I
for b3 being set holds
( b3 = Bool M iff for x being set holds
( x in b3 iff x is ManySortedSubset of M ) );

registration
let I be set ;
let M be ManySortedSet of I;
cluster Bool M ->  non empty functional with_common_domain ;
coherence
 ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain )
proofend;
end;

definition
let I be set ;
let M be ManySortedSet of I;
mode SubsetFamily of M is Subset of (Bool M);
end;

definition
let I be set ;
let M be ManySortedSet of I;
:: original:Bool
redefine func Bool M ->  SubsetFamily of M;
coherence
 Bool M is SubsetFamily of M
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster non empty functional with_common_domain for Element of bool (Bool M);
existence
 ex b1 being SubsetFamily of M st
( not b1 is empty & b1 is functional & b1 is with_common_domain )
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster empty functional finite for Element of bool (Bool M);
existence
 ex b1 being SubsetFamily of M st
( b1 is empty & b1 is finite )
proofend;
end;

definition
let I be set ;
let M be ManySortedSet of I;
let S be non empty SubsetFamily of M;
:: original:Element
redefine mode Element of S ->  ManySortedSubset of M;
coherence
 for b1 being Element of S holds b1 is ManySortedSubset of M
proofend;
end;

theorem Th3: :: CLOSURE2:3
for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF \/ SG is SubsetFamily of M ;

theorem :: CLOSURE2:4
for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF /\ SG is SubsetFamily of M ;

theorem :: CLOSURE2:5
for I, x being set
for M being ManySortedSet of I
for SF being SubsetFamily of M holds SF \ x is SubsetFamily of M ;

theorem :: CLOSURE2:6
for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF \+\ SG is SubsetFamily of M ;

theorem Th7: :: CLOSURE2:7
for I being set
for A, M being ManySortedSet of I st A c= M holds
{A} is SubsetFamily of M
proofend;

theorem Th8: :: CLOSURE2:8
for I being set
for A, M, B being ManySortedSet of I st A c= M & B c= M holds
{A,B} is SubsetFamily of M
proofend;

theorem Th9: :: CLOSURE2:9
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E /\ T in Bool M
proofend;

theorem Th10: :: CLOSURE2:10
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E \/ T in Bool M
proofend;

theorem :: CLOSURE2:11
for I being set
for A, M being ManySortedSet of I
for E being Element of Bool M holds E \ A in Bool M
proofend;

theorem :: CLOSURE2:12
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E \+\ T in Bool M
proofend;

begin

:: to the Operator on Many Sorted Subsets
definition
let S be functional set ;
func|.S.| ->  Function means :Def2: :: CLOSURE2:def 2
 ex A being non empty functional set st
( A = S & dom it = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom it holds
it . i =  {  (x . i) where x is Element of A : verum  }  ) ) if S <> {}
otherwise it = {} ;
existence
 ( ( S <> {} implies ex b1 being Function ex A being non empty functional set st
( A = S &amp; dom b1 = meet  {  (dom x) where x is Element of A : verum  }  &amp; ( for i being set st i in dom b1 holds
b1 . i =  {  (x . i) where x is Element of A : verum  }  ) ) ) &amp; ( not S <> {} implies ex b1 being Function st b1 = {} ) )
proofend;
uniqueness
 for b1, b2 being Function holds
( ( S <> {} &amp; ex A being non empty functional set st
( A = S &amp; dom b1 = meet  {  (dom x) where x is Element of A : verum  }  &amp; ( for i being set st i in dom b1 holds
b1 . i =  {  (x . i) where x is Element of A : verum  }  ) ) &amp; ex A being non empty functional set st
( A = S &amp; dom b2 = meet  {  (dom x) where x is Element of A : verum  }  &amp; ( for i being set st i in dom b2 holds
b2 . i =  {  (x . i) where x is Element of A : verum  }  ) ) implies b1 = b2 ) &amp; ( not S <> {} &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) )
proofend;
consistency
 for b1 being Function holds verum ;
end;

:: deftheorem Def2 defines |. CLOSURE2:def_2_:_
 for S being functional set
for b2 being Function holds
( ( S <> {} implies ( b2 = |.S.| iff ex A being non empty functional set st
( A = S &amp; dom b2 = meet  {  (dom x) where x is Element of A : verum  }  &amp; ( for i being set st i in dom b2 holds
b2 . i =  {  (x . i) where x is Element of A : verum  }  ) ) ) ) &amp; ( not S <> {} implies ( b2 = |.S.| iff b2 = {} ) ) );

theorem Th13: :: CLOSURE2:13
for I being set
for M being ManySortedSet of I
for SF being non empty SubsetFamily of M holds dom |.SF.| = I
proofend;

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

definition
let I be set ;
let M be ManySortedSet of I;
let S be SubsetFamily of M;
func|:S:| ->  ManySortedSet of I equals :Def3: :: CLOSURE2:def 3
|.S.| if S <> {}
otherwise  [[0]] I;
coherence
 ( ( S <> {} implies |.S.| is ManySortedSet of I ) &amp; ( not S <> {} implies [[0]] I is ManySortedSet of I ) )
proofend;
consistency
 for b1 being ManySortedSet of I holds verum ;
end;

:: deftheorem Def3 defines |: CLOSURE2:def_3_:_
 for I being set
for M being ManySortedSet of I
for S being SubsetFamily of M holds
( ( S <> {} implies |:S:| = |.S.| ) &amp; ( not S <> {} implies |:S:| = [[0]] I ) );

registration
let I be set ;
let M be ManySortedSet of I;
let S be empty SubsetFamily of M;
cluster|:S:| -> V9() ;
coherence
 |:S:| is empty-yielding
proofend;
end;

theorem Th14: :: CLOSURE2:14
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }
proofend;

registration
let I be set ;
let M be ManySortedSet of I;
let SF be non empty SubsetFamily of M;
cluster|:SF:| -> V8() ;
coherence
 |:SF:| is non-empty
proofend;
end;

theorem Th15: :: CLOSURE2:15
for f being Function holds dom |.{f}.| = dom f
proofend;

theorem :: CLOSURE2:16
for f, f1 being Function holds dom |.{f,f1}.| = (dom f) /\ (dom f1)
proofend;

theorem Th17: :: CLOSURE2:17
for i being set
for f being Function st i in dom f holds
|.{f}.| . i = {(f . i)}
proofend;

theorem :: CLOSURE2:18
for i, I being set
for M being ManySortedSet of I
for f being Function
for SF being SubsetFamily of M st i in I &amp; SF = {f} holds
|:SF:| . i = {(f . i)}
proofend;

theorem Th19: :: CLOSURE2:19
for i being set
for f, f1 being Function st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = {(f . i),(f1 . i)}
proofend;

theorem Th20: :: CLOSURE2:20
for i, I being set
for M being ManySortedSet of I
for f, f1 being Function
for SF being SubsetFamily of M st i in I &amp; SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
let SF be SubsetFamily of M;
:: original:|:
redefine func|:SF:| ->  MSSubsetFamily of M;
coherence
 |:SF:| is MSSubsetFamily of M
proofend;
end;

theorem Th21: :: CLOSURE2:21
for I being set
for M, A being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
proofend;

theorem Th22: :: CLOSURE2:22
for I being set
for M, A, B being ManySortedSet of I
for SF being SubsetFamily of M st SF = {A,B} holds
union |:SF:| = A \/ B
proofend;

theorem Th23: :: CLOSURE2:23
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
proofend;

theorem Th24: :: CLOSURE2:24
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
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:|
proofend;

theorem :: CLOSURE2:25
for I being set
for M being ManySortedSet of I holds |:(Bool M):| = bool M
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
let IT be SubsetFamily of M;
attrIT is additive  means :: CLOSURE2:def 4
 for A, B being ManySortedSet of I st A in IT &amp; B in IT holds
A \/ B in IT;
attrIT is absolutely-additive  means :Def5: :: CLOSURE2:def 5
 for F being SubsetFamily of M st F c= IT holds
union |:F:| in IT;
attrIT is multiplicative  means :: CLOSURE2:def 6
 for A, B being ManySortedSet of I st A in IT &amp; B in IT holds
A /\ B in IT;
attrIT is absolutely-multiplicative  means :Def7: :: CLOSURE2:def 7
 for F being SubsetFamily of M st F c= IT holds
meet |:F:| in IT;
attrIT is properly-upper-bound  means :Def8: :: CLOSURE2:def 8
M in IT;
attrIT is properly-lower-bound  means :Def9: :: CLOSURE2:def 9
 [[0]] I in IT;
end;

:: deftheorem  defines additive CLOSURE2:def_4_:_
 for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is additive iff for A, B being ManySortedSet of I st A in IT &amp; B in IT holds
A \/ B in IT );

:: deftheorem Def5 defines absolutely-additive CLOSURE2:def_5_:_
 for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is absolutely-additive iff for F being SubsetFamily of M st F c= IT holds
union |:F:| in IT );

:: deftheorem  defines multiplicative CLOSURE2:def_6_:_
 for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is multiplicative iff for A, B being ManySortedSet of I st A in IT &amp; B in IT holds
A /\ B in IT );

:: deftheorem Def7 defines absolutely-multiplicative CLOSURE2:def_7_:_
 for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is absolutely-multiplicative iff for F being SubsetFamily of M st F c= IT holds
meet |:F:| in IT );

:: deftheorem Def8 defines properly-upper-bound CLOSURE2:def_8_:_
 for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is properly-upper-bound iff M in IT );

:: deftheorem Def9 defines properly-lower-bound CLOSURE2:def_9_:_
 for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is properly-lower-bound iff [[0]] I in IT );

Lm1:  for I being set
for M being ManySortedSet of I holds
( Bool M is additive &amp; Bool M is absolutely-additive &amp; Bool M is multiplicative &amp; Bool M is absolutely-multiplicative &amp; Bool M is properly-upper-bound &amp; Bool M is properly-lower-bound )
proofend;

registration
let I be set ;
let M be ManySortedSet of I;
cluster non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for Element of bool (Bool M);
existence
 ex b1 being SubsetFamily of M st
( not b1 is empty &amp; b1 is functional &amp; b1 is with_common_domain &amp; b1 is additive &amp; b1 is absolutely-additive &amp; b1 is multiplicative &amp; b1 is absolutely-multiplicative &amp; b1 is properly-upper-bound &amp; b1 is properly-lower-bound )
proofend;
end;

definition
let I be set ;
let M be ManySortedSet of I;
:: original:Bool
redefine func Bool M ->  additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M;
coherence
 Bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M by Lm1;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive  ->  additive for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is absolutely-additive holds
b1 is additive
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative  ->  multiplicative for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is multiplicative
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative  ->  properly-upper-bound for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster properly-upper-bound  ->  non empty for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is properly-upper-bound holds
not b1 is empty by Def8;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive  ->  properly-lower-bound for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is absolutely-additive holds
b1 is properly-lower-bound
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster properly-lower-bound  ->  non empty for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is properly-lower-bound holds
not b1 is empty by Def9;
end;

begin

definition
let I be set ;
let M be ManySortedSet of I;
mode SetOp of M is Function of (Bool M),(Bool M);
end;

definition
let I be set ;
let M be ManySortedSet of I;
let f be SetOp of M;
let x be Element of Bool M;
:: original:.
redefine funcf . x ->  Element of Bool M;
coherence
 f . x is Element of Bool M
proofend;
end;

definition
let I be set ;
let M be ManySortedSet of I;
let IT be SetOp of M;
attrIT is reflexive  means :Def10: :: CLOSURE2:def 10
 for x being Element of Bool M holds x c=' IT . x;
attrIT is monotonic  means :Def11: :: CLOSURE2:def 11
 for x, y being Element of Bool M st x c=' y holds
IT . x c=' IT . y;
attrIT is idempotent  means :Def12: :: CLOSURE2:def 12
 for x being Element of Bool M holds IT . x = IT . (IT . x);
attrIT is topological  means :Def13: :: CLOSURE2:def 13
 for x, y being Element of Bool M holds IT . (x \/ y) = (IT . x) \/ (IT . y);
end;

:: deftheorem Def10 defines reflexive CLOSURE2:def_10_:_
 for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is reflexive iff for x being Element of Bool M holds x c=' IT . x );

:: deftheorem Def11 defines monotonic CLOSURE2:def_11_:_
 for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is monotonic iff for x, y being Element of Bool M st x c=' y holds
IT . x c=' IT . y );

:: deftheorem Def12 defines idempotent CLOSURE2:def_12_:_
 for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is idempotent iff for x being Element of Bool M holds IT . x = IT . (IT . x) );

:: deftheorem Def13 defines topological CLOSURE2:def_13_:_
 for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is topological iff for x, y being Element of Bool M holds IT . (x \/ y) = (IT . x) \/ (IT . y) );

registration
let I be set ;
let M be ManySortedSet of I;
cluster non empty Relation-like Function-like V17( Bool M) quasi_total reflexive monotonic idempotent topological for Element of bool [:(Bool M),(Bool M):];
existence
 ex b1 being SetOp of M st
( b1 is reflexive &amp; b1 is monotonic &amp; b1 is idempotent &amp; b1 is topological )
proofend;
end;

theorem :: CLOSURE2:26
for I being set
for A being ManySortedSet of I holds id (Bool A) is reflexive SetOp of A
proofend;

theorem :: CLOSURE2:27
for I being set
for A being ManySortedSet of I holds id (Bool A) is monotonic SetOp of A
proofend;

theorem :: CLOSURE2:28
for I being set
for A being ManySortedSet of I holds id (Bool A) is idempotent SetOp of A
proofend;

theorem :: CLOSURE2:29
for I being set
for A being ManySortedSet of I holds id (Bool A) is topological SetOp of A
proofend;

theorem :: CLOSURE2:30
for I being set
for M being ManySortedSet of I
for E being Element of Bool M
for g being SetOp of M st E = M &amp; g is reflexive holds
E = g . E
proofend;

theorem :: CLOSURE2:31
for I being set
for M being ManySortedSet of I
for g being SetOp of M st g is reflexive &amp; ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
proofend;

theorem :: CLOSURE2:32
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E /\ T &amp; g is monotonic holds
g . A c= (g . E) /\ (g . T)
proofend;

registration
let I be set ;
let M be ManySortedSet of I;
cluster Function-like quasi_total topological  ->  monotonic for Element of bool [:(Bool M),(Bool M):];
coherence
 for b1 being SetOp of M st b1 is topological holds
b1 is monotonic
proofend;
end;

theorem :: CLOSURE2:33
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E \ T &amp; g is topological holds
(g . E) \ (g . T) c= g . A
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
let h, g be SetOp of M;
:: original:*
redefine funcg * h ->  SetOp of M;
coherence
 h * g is SetOp of M
proofend;
end;

theorem :: CLOSURE2:34
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is reflexive &amp; h is reflexive holds
g * h is reflexive
proofend;

theorem :: CLOSURE2:35
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is monotonic &amp; h is monotonic holds
g * h is monotonic
proofend;

theorem :: CLOSURE2:36
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is idempotent &amp; h is idempotent &amp; g * h = h * g holds
g * h is idempotent
proofend;

theorem :: CLOSURE2:37
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is topological &amp; h is topological holds
g * h is topological
proofend;

begin

definition
let S be 1-sorted ;
attrc2 is strict ;
struct ClosureStr over S ->  many-sorted over S;
aggrClosureStr(# Sorts, Family #) ->  ClosureStr over S;
sel Family c2 ->  SubsetFamily of the Sorts of c2;
end;

definition
let S be 1-sorted ;
let IT be ClosureStr over S;
attrIT is additive  means :Def14: :: CLOSURE2:def 14
 the Family of IT is additive ;
attrIT is absolutely-additive  means :Def15: :: CLOSURE2:def 15
 the Family of IT is absolutely-additive ;
attrIT is multiplicative  means :Def16: :: CLOSURE2:def 16
 the Family of IT is multiplicative ;
attrIT is absolutely-multiplicative  means :Def17: :: CLOSURE2:def 17
 the Family of IT is absolutely-multiplicative ;
attrIT is properly-upper-bound  means :Def18: :: CLOSURE2:def 18
 the Family of IT is properly-upper-bound ;
attrIT is properly-lower-bound  means :Def19: :: CLOSURE2:def 19
 the Family of IT is properly-lower-bound ;
end;

:: deftheorem Def14 defines additive CLOSURE2:def_14_:_
 for S being 1-sorted
for IT being ClosureStr over S holds
( IT is additive iff the Family of IT is additive );

:: deftheorem Def15 defines absolutely-additive CLOSURE2:def_15_:_
 for S being 1-sorted
for IT being ClosureStr over S holds
( IT is absolutely-additive iff the Family of IT is absolutely-additive );

:: deftheorem Def16 defines multiplicative CLOSURE2:def_16_:_
 for S being 1-sorted
for IT being ClosureStr over S holds
( IT is multiplicative iff the Family of IT is multiplicative );

:: deftheorem Def17 defines absolutely-multiplicative CLOSURE2:def_17_:_
 for S being 1-sorted
for IT being ClosureStr over S holds
( IT is absolutely-multiplicative iff the Family of IT is absolutely-multiplicative );

:: deftheorem Def18 defines properly-upper-bound CLOSURE2:def_18_:_
 for S being 1-sorted
for IT being ClosureStr over S holds
( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );

:: deftheorem Def19 defines properly-lower-bound CLOSURE2:def_19_:_
 for S being 1-sorted
for IT being ClosureStr over S holds
( IT is properly-lower-bound iff the Family of IT is properly-lower-bound );

definition
let S be 1-sorted ;
let MS be many-sorted over S;
func Full MS ->  ClosureStr over S equals :: CLOSURE2:def 20
 ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #);
correctness
coherence
ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #) is ClosureStr over S;
;
end;

:: deftheorem  defines Full CLOSURE2:def_20_:_
 for S being 1-sorted
for MS being many-sorted over S holds Full MS = ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #);

registration
let S be 1-sorted ;
let MS be many-sorted over S;
cluster Full MS ->  strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence
 ( Full MS is strict &amp; Full MS is additive &amp; Full MS is absolutely-additive &amp; Full MS is multiplicative &amp; Full MS is absolutely-multiplicative &amp; Full MS is properly-upper-bound &amp; Full MS is properly-lower-bound )
proofend;
end;

registration
let S be 1-sorted ;
let MS be non-empty many-sorted over S;
cluster Full MS ->  non-empty ;
coherence
 Full MS is non-empty by MSUALG_1:def_3;
end;

registration
let S be 1-sorted ;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ClosureStr over S;
existence
 ex b1 being ClosureStr over S st
( b1 is strict &amp; b1 is non-empty &amp; b1 is additive &amp; b1 is absolutely-additive &amp; b1 is multiplicative &amp; b1 is absolutely-multiplicative &amp; b1 is properly-upper-bound &amp; b1 is properly-lower-bound )
proofend;
end;

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

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

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

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

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

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

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

registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be additive SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) ->  additive ;
coherence
 ClosureStr(# the Sorts of MS,F #) is additive by Def14;
end;

registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be absolutely-additive SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) ->  absolutely-additive ;
coherence
 ClosureStr(# the Sorts of MS,F #) is absolutely-additive by Def15;
end;

registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) ->  multiplicative ;
coherence
 ClosureStr(# the Sorts of MS,F #) is multiplicative by Def16;
end;

registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be absolutely-multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) ->  absolutely-multiplicative ;
coherence
 ClosureStr(# the Sorts of MS,F #) is absolutely-multiplicative by Def17;
end;

registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be properly-upper-bound SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) ->  properly-upper-bound ;
coherence
 ClosureStr(# the Sorts of MS,F #) is properly-upper-bound by Def18;
end;

registration
let S be 1-sorted ;
let MS be many-sorted over S;
let F be properly-lower-bound SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) ->  properly-lower-bound ;
coherence
 ClosureStr(# the Sorts of MS,F #) is properly-lower-bound by Def19;
end;

registration
let S be 1-sorted ;
cluster absolutely-additive  ->  additive for ClosureStr over S;
coherence
 for b1 being ClosureStr over S st b1 is absolutely-additive holds
b1 is additive
proofend;
end;

registration
let S be 1-sorted ;
cluster absolutely-multiplicative  ->  multiplicative for ClosureStr over S;
coherence
 for b1 being ClosureStr over S st b1 is absolutely-multiplicative holds
b1 is multiplicative
proofend;
end;

registration
let S be 1-sorted ;
cluster absolutely-multiplicative  ->  properly-upper-bound for ClosureStr over S;
coherence
 for b1 being ClosureStr over S st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proofend;
end;

registration
let S be 1-sorted ;
cluster absolutely-additive  ->  properly-lower-bound for ClosureStr over S;
coherence
 for b1 being ClosureStr over S st b1 is absolutely-additive holds
b1 is properly-lower-bound
proofend;
end;

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

definition
let I be set ;
let M be ManySortedSet of I;
mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M;
end;

definition
let S be 1-sorted ;
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: :: CLOSURE2:def 21
( the Sorts of it = A &amp; the Family of it =  {  x where x is Element of Bool A : g . x = x  }  );
existence
 ex b1 being strict ClosureStr over S st
( the Sorts of b1 = A &amp; the Family of b1 =  {  x where x is Element of Bool A : g . x = x  }  )
proofend;
uniqueness
 for b1, b2 being strict ClosureStr over S st the Sorts of b1 = A &amp; the Family of b1 =  {  x where x is Element of Bool A : g . x = x  }  &amp; the Sorts of b2 = A &amp; the Family of b2 =  {  x where x is Element of Bool A : g . x = x  }  holds
b1 = b2 ;
end;

:: deftheorem Def21 defines ClOp->ClSys CLOSURE2:def_21_:_
 for S being 1-sorted
for A being ManySortedSet of the carrier of S
for g being ClosureOperator of A
for b4 being strict ClosureStr over S holds
( b4 = ClOp->ClSys g iff ( the Sorts of b4 = A &amp; the Family of b4 =  {  x where x is Element of Bool A : g . x = x  }  ) );

registration
let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;
cluster ClOp->ClSys g ->  strict absolutely-multiplicative ;
coherence
 ClOp->ClSys g is absolutely-multiplicative
proofend;
end;

definition
let S be 1-sorted ;
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: :: CLOSURE2:def 22
 ex F being SubsetFamily of the Sorts of A st
( it = meet |:F:| &amp; F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X &amp; X in the Family of A )  }  );
existence
 ex b1 being Element of Bool the Sorts of A ex F being SubsetFamily of the Sorts of A st
( b1 = meet |:F:| &amp; F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X &amp; X in the Family of A )  }  )
proofend;
uniqueness
 for b1, b2 being Element of Bool the Sorts of A st ex F being SubsetFamily of the Sorts of A st
( b1 = meet |:F:| &amp; F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X &amp; X in the Family of A )  }  ) &amp; ex F being SubsetFamily of the Sorts of A st
( b2 = meet |:F:| &amp; F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X &amp; X in the Family of A )  }  ) holds
b1 = b2 ;
end;

:: deftheorem Def22 defines Cl CLOSURE2:def_22_:_
 for S being 1-sorted
for A being ClosureSystem of S
for C being ManySortedSubset of the Sorts of A
for b4 being Element of Bool the Sorts of A holds
( b4 = Cl C iff ex F being SubsetFamily of the Sorts of A st
( b4 = meet |:F:| &amp; F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X &amp; X in the Family of A )  }  ) );

theorem Th38: :: CLOSURE2:38
for S being 1-sorted
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 &amp; ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a
proofend;

theorem :: CLOSURE2:39
for S being 1-sorted
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 &amp; ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
proofend;

theorem Th40: :: CLOSURE2:40
for S being 1-sorted
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 &amp; f is monotonic &amp; f is idempotent )
proofend;

definition
let S be 1-sorted ;
let D be ClosureSystem of S;
func ClSys->ClOp D ->  ClosureOperator of the Sorts of D means :Def23: :: CLOSURE2:def 23
 for x being Element of Bool the Sorts of D holds it . x = Cl x;
existence
 ex b1 being ClosureOperator of the Sorts of D st
for x being Element of Bool the Sorts of D holds b1 . x = Cl x
proofend;
uniqueness
 for b1, b2 being ClosureOperator of the Sorts of D st ( for x being Element of Bool the Sorts of D holds b1 . x = Cl x ) &amp; ( for x being Element of Bool the Sorts of D holds b2 . x = Cl x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def23 defines ClSys->ClOp CLOSURE2:def_23_:_
 for S being 1-sorted
for D being ClosureSystem of S
for b3 being ClosureOperator of the Sorts of D holds
( b3 = ClSys->ClOp D iff for x being Element of Bool the Sorts of D holds b3 . x = Cl x );

theorem :: CLOSURE2:41
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
proofend;

deffunc H1( set ) ->  set = $1;

theorem :: CLOSURE2:42
for S being 1-sorted
for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)
proofend;