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


begin

scheme :: CLOSURE1:sch 1
MSSUBSET{ F1() ->  set , F2() ->  V8() ManySortedSet of F1(), F3() ->  ManySortedSet of F1(), P1[ set ] } :
 ( ( for X being ManySortedSet of F1() holds
( X in F2() iff ( X in F3() & P1[X] ) ) ) implies F2() c= F3() )
proofend;

theorem Th1: :: CLOSURE1:1
for X being non empty set
for x, y being set st x c= y holds
{  t where t is Element of X : y c= t  }  c=  {  z where z is Element of X : x c= z  }
proofend;

theorem :: CLOSURE1:2
for I being set
for M being ManySortedSet of I st ex A being ManySortedSet of I st A in M holds
M is V8()
proofend;

registration
let I be set ;
let F be ManySortedFunction of I;
let A be ManySortedSet of I;
clusterF .. A -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = F .. A holds
b1 is total ;
end;

Lm1: now__::_thesis:_for_I_being_set_
for_A,_B_being_V8()_ManySortedSet_of_I
for_F_being_ManySortedFunction_of_A,B
for_X_being_Element_of_A_holds_F_.._X_is_Element_of_B
let I be set ; ::_thesis: for A, B being V8() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being Element of A holds F .. X is Element of B
let A, B be V8() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B
for X being Element of A holds F .. X is Element of B
let F be ManySortedFunction of A,B; ::_thesis: for X being Element of A holds F .. X is Element of B
let X be Element of A; ::_thesis: F .. X is Element of B
thus  F .. X is Element of B ::_thesis: verum
proof
let i be set ; :: according toPBOOLE:def_14 ::_thesis: ( not i in I or (F .. X) . i is Element of B . i )
assume A1: i in I ; ::_thesis: (F .. X) . i is Element of B . i
reconsider g = F . i as Function ;
 ( g is Function of (A . i),(B . i) & X . i is Element of A . i ) by A1, PBOOLE:def_14, PBOOLE:def_15;
then  ( dom F = I & g . (X . i) in B . i ) by A1, FUNCT_2:5, PARTFUN1:def_2;
hence  (F .. X) . i is Element of B . i by A1, PRALG_1:def_17; ::_thesis: verum
end;
end;

definition
let I be set ;
let A, B be V8() ManySortedSet of I;
let F be ManySortedFunction of A,B;
let X be Element of A;
:: original:..
redefine funcF .. X ->  Element of B;
coherence
 F .. X is Element of B by Lm1;
end;

theorem :: CLOSURE1:3
for I being set
for A, X being ManySortedSet of I
for B being V8() ManySortedSet of I
for F being ManySortedFunction of A,B st X in A holds
F .. X in B
proofend;

theorem Th4: :: CLOSURE1:4
for I being set
for F, G being ManySortedFunction of I
for A being ManySortedSet of I st A in doms G holds
F .. (G .. A) = (F ** G) .. A
proofend;

theorem :: CLOSURE1:5
for I being set
for F being ManySortedFunction of I st F is "1-1" holds
for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B
proofend;

theorem :: CLOSURE1:6
for I being set
for F being ManySortedFunction of I st doms F is V8() & ( for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B ) holds
F is "1-1"
proofend;

theorem Th7: :: CLOSURE1:7
for I being set
for A, B being V8() ManySortedSet of I
for F, G being ManySortedFunction of A,B st ( for M being ManySortedSet of I st M in A holds
F .. M = G .. M ) holds
F = G
proofend;

registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like V9() I -defined Function-like total V42() for Element of bool M;
existence
 ex b1 being Element of bool M st
( b1 is V9() & b1 is V42() )
proofend;
end;

begin

definition
let I be set ;
let M be ManySortedSet of I;
mode MSSetOp of M is ManySortedFunction of bool M, bool M;
end;

definition
let I be set ;
let M be ManySortedSet of I;
let O be MSSetOp of M;
let X be Element of bool M;
:: original:..
redefine funcO .. X ->  Element of bool M;
coherence
 O .. X is Element of bool M by Lm1;
end;

definition
let I be set ;
let M be ManySortedSet of I;
let IT be MSSetOp of M;
attrIT is reflexive  means :Def1: :: CLOSURE1:def 1
 for X being Element of bool M holds X c= IT .. X;
attrIT is monotonic  means :Def2: :: CLOSURE1:def 2
 for X, Y being Element of bool M st X c= Y holds
IT .. X c= IT .. Y;
attrIT is idempotent  means :Def3: :: CLOSURE1:def 3
 for X being Element of bool M holds IT .. X = IT .. (IT .. X);
attrIT is topological  means :Def4: :: CLOSURE1:def 4
 for X, Y being Element of bool M holds IT .. (X \/ Y) = (IT .. X) \/ (IT .. Y);
end;

:: deftheorem Def1 defines reflexive CLOSURE1:def_1_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSetOp of M holds
( IT is reflexive iff for X being Element of bool M holds X c= IT .. X );

:: deftheorem Def2 defines monotonic CLOSURE1:def_2_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSetOp 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 Def3 defines idempotent CLOSURE1:def_3_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSetOp of M holds
( IT is idempotent iff for X being Element of bool M holds IT .. X = IT .. (IT .. X) );

:: deftheorem Def4 defines topological CLOSURE1:def_4_:_
 for I being set
for M being ManySortedSet of I
for IT being MSSetOp of M holds
( IT is topological iff for X, Y being Element of bool M holds IT .. (X \/ Y) = (IT .. X) \/ (IT .. Y) );

theorem Th8: :: CLOSURE1:8
for I being set
for M being V8() ManySortedSet of I
for X being Element of M holds X = (id M) .. X
proofend;

theorem Th9: :: CLOSURE1:9
for I being set
for M being V8() ManySortedSet of I
for X, Y being Element of M st X c= Y holds
(id M) .. X c= (id M) .. Y
proofend;

theorem Th10: :: CLOSURE1:10
for I being set
for M being V8() ManySortedSet of I
for X, Y being Element of M st X \/ Y is Element of M holds
(id M) .. (X \/ Y) = ((id M) .. X) \/ ((id M) .. Y)
proofend;

theorem :: CLOSURE1:11
for I being set
for M being ManySortedSet of I
for X being Element of bool M
for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being V42() Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
proofend;

registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like I -defined Function-like total Function-yielding V25() reflexive monotonic idempotent topological for ManySortedFunction of bool M, bool M;
existence
 ex b1 being MSSetOp of M st
( b1 is reflexive & b1 is monotonic & b1 is idempotent & b1 is topological )
proofend;
end;

theorem :: CLOSURE1:12
for I being set
for A being ManySortedSet of I holds id (bool A) is reflexive MSSetOp of A
proofend;

theorem :: CLOSURE1:13
for I being set
for A being ManySortedSet of I holds id (bool A) is monotonic MSSetOp of A
proofend;

theorem :: CLOSURE1:14
for I being set
for A being ManySortedSet of I holds id (bool A) is idempotent MSSetOp of A
proofend;

theorem :: CLOSURE1:15
for I being set
for A being ManySortedSet of I holds id (bool A) is topological MSSetOp of A
proofend;

theorem :: CLOSURE1:16
for I being set
for M being ManySortedSet of I
for P being MSSetOp of M
for E being Element of bool M st E = M & P is reflexive holds
E = P .. E
proofend;

theorem :: CLOSURE1:17
for I being set
for M being ManySortedSet of I
for P being MSSetOp of M st P is reflexive & ( for X being Element of bool M holds P .. X c= X ) holds
P is idempotent
proofend;

theorem :: CLOSURE1:18
for I being set
for M being ManySortedSet of I
for P being MSSetOp of M
for E, T being Element of bool M st P is monotonic holds
P .. (E /\ T) c= (P .. E) /\ (P .. T)
proofend;

registration
let I be set ;
let M be ManySortedSet of I;
cluster topological  ->  monotonic for ManySortedFunction of bool M, bool M;
coherence
 for b1 being MSSetOp of M st b1 is topological holds
b1 is monotonic
proofend;
end;

theorem :: CLOSURE1:19
for I being set
for M being ManySortedSet of I
for P being MSSetOp of M
for E, T being Element of bool M st P is topological holds
(P .. E) \ (P .. T) c= P .. (E \ T)
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
let R, P be MSSetOp of M;
:: original:**
redefine funcP ** R ->  MSSetOp of M;
coherence
 P ** R is MSSetOp of M
proofend;
end;

theorem :: CLOSURE1:20
for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is reflexive & R is reflexive holds
P ** R is reflexive
proofend;

theorem :: CLOSURE1:21
for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is monotonic & R is monotonic holds
P ** R is monotonic
proofend;

theorem :: CLOSURE1:22
for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is idempotent & R is idempotent & P ** R = R ** P holds
P ** R is idempotent
proofend;

theorem :: CLOSURE1:23
for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is topological & R is topological holds
P ** R is topological
proofend;

Lm2: now__::_thesis:_for_I_being_set_
for_M_being_ManySortedSet_of_I
for_i_being_set_
for_a_being_ManySortedSet_of_I
for_b_being_Element_of_bool_(M_._i)_st_a_=_([[0]]_I)_+*_(i_.-->_b)_holds_
a_in_bool_M
let I be set ; ::_thesis: for M being ManySortedSet of I
for i being set
for a being ManySortedSet of I
for b being Element of bool (M . i) st a = ([[0]] I) +* (i .--> b) holds
a in bool M
let M be ManySortedSet of I; ::_thesis: for i being set
for a being ManySortedSet of I
for b being Element of bool (M . i) st a = ([[0]] I) +* (i .--> b) holds
a in bool M
let i be set ; ::_thesis: for a being ManySortedSet of I
for b being Element of bool (M . i) st a = ([[0]] I) +* (i .--> b) holds
a in bool M
let a be ManySortedSet of I; ::_thesis: for b being Element of bool (M . i) st a = ([[0]] I) +* (i .--> b) holds
a in bool M
let b be Element of bool (M . i); ::_thesis: ( a = ([[0]] I) +* (i .--> b) implies a in bool M )
assume A1: a = ([[0]] I) +* (i .--> b) ; ::_thesis: a in bool M
A2: dom (i .--> b) = {i} by FUNCOP_1:13;
 [[0]] I c= M by MBOOLEAN:5;
then A3: [[0]] I in bool M by MBOOLEAN:1;
thus  a in bool M ::_thesis: verum
proof
let j be set ; :: according toPBOOLE:def_1 ::_thesis: ( not j in I or a . j in (bool M) . j )
assume A4: j in I ; ::_thesis: a . j in (bool M) . j
 i in {i} by TARSKI:def_1;
then A5: a . i = (i .--> b) . i by A1, A2, FUNCT_4:13
.= b by FUNCOP_1:72 ;
now__::_thesis:_(_(_j_=_i_&amp;_a_._j_in_(bool_M)_._j_)_or_(_j_<>_i_&amp;_a_._j_in_(bool_M)_._j_)_)
percases ( j = i or j <> i ) ;
caseA6: j = i ; ::_thesis: a . j in (bool M) . j
then  b in bool (M . j) ;
hence  a . j in (bool M) . j by A4, A5, A6, MBOOLEAN:def_1; ::_thesis: verum
end;
case j <> i ; ::_thesis: a . j in (bool M) . j
then  not j in dom (i .--> b) by A2, TARSKI:def_1;
then  a . j = ([[0]] I) . j by A1, FUNCT_4:11;
hence  a . j in (bool M) . j by A3, A4, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  a . j in (bool M) . j ; ::_thesis: verum
end;
end;

theorem Th24: :: CLOSURE1:24
for i, I being set
for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is reflexive &amp; i in I &amp; f = P . i holds
for x being Element of bool (M . i) holds x c= f . x
proofend;

theorem Th25: :: CLOSURE1:25
for i, I being set
for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is monotonic &amp; i in I &amp; f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
proofend;

theorem Th26: :: CLOSURE1:26
for i, I being set
for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is idempotent &amp; i in I &amp; f = P . i holds
for x being Element of bool (M . i) holds f . x = f . (f . x)
proofend;

theorem :: CLOSURE1:27
for i, I being set
for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is topological &amp; i in I &amp; f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
proofend;

begin

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

definition
let S be 1-sorted ;
let IT be MSClosureStr over S;
attrIT is additive  means :Def5: :: CLOSURE1:def 5
 the Family of IT is additive ;
attrIT is absolutely-additive  means :Def6: :: CLOSURE1:def 6
 the Family of IT is absolutely-additive ;
attrIT is multiplicative  means :Def7: :: CLOSURE1:def 7
 the Family of IT is multiplicative ;
attrIT is absolutely-multiplicative  means :Def8: :: CLOSURE1:def 8
 the Family of IT is absolutely-multiplicative ;
attrIT is properly-upper-bound  means :Def9: :: CLOSURE1:def 9
 the Family of IT is properly-upper-bound ;
attrIT is properly-lower-bound  means :Def10: :: CLOSURE1:def 10
 the Family of IT is properly-lower-bound ;
end;

:: deftheorem Def5 defines additive CLOSURE1:def_5_:_
 for S being 1-sorted
for IT being MSClosureStr over S holds
( IT is additive iff the Family of IT is additive );

:: deftheorem Def6 defines absolutely-additive CLOSURE1:def_6_:_
 for S being 1-sorted
for IT being MSClosureStr over S holds
( IT is absolutely-additive iff the Family of IT is absolutely-additive );

:: deftheorem Def7 defines multiplicative CLOSURE1:def_7_:_
 for S being 1-sorted
for IT being MSClosureStr over S holds
( IT is multiplicative iff the Family of IT is multiplicative );

:: deftheorem Def8 defines absolutely-multiplicative CLOSURE1:def_8_:_
 for S being 1-sorted
for IT being MSClosureStr over S holds
( IT is absolutely-multiplicative iff the Family of IT is absolutely-multiplicative );

:: deftheorem Def9 defines properly-upper-bound CLOSURE1:def_9_:_
 for S being 1-sorted
for IT being MSClosureStr over S holds
( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );

:: deftheorem Def10 defines properly-lower-bound CLOSURE1:def_10_:_
 for S being 1-sorted
for IT being MSClosureStr 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 MSFull MS ->  MSClosureStr over S equals :: CLOSURE1:def 11
 MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);
correctness
coherence
MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #) is MSClosureStr over S;
;
end;

:: deftheorem  defines MSFull CLOSURE1:def_11_:_
 for S being 1-sorted
for MS being many-sorted over S holds MSFull MS = MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);

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

registration
let S be 1-sorted ;
let MS be non-empty many-sorted over S;
cluster MSFull MS ->  non-empty ;
coherence
 MSFull 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 MSClosureStr over S;
existence
 ex b1 being MSClosureStr 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 MSClosureStr over S;
cluster the Family of CS ->  additive ;
coherence
 the Family of CS is additive by Def5;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

registration
let S be 1-sorted ;
cluster absolutely-multiplicative  ->  multiplicative for MSClosureStr over S;
coherence
 for b1 being MSClosureStr 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 MSClosureStr over S;
coherence
 for b1 being MSClosureStr 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 MSClosureStr over S;
coherence
 for b1 being MSClosureStr over S st b1 is absolutely-additive holds
b1 is properly-lower-bound
proofend;
end;

definition
let S be 1-sorted ;
mode MSClosureSystem of S is absolutely-multiplicative MSClosureStr over S;
end;

definition
let I be set ;
let M be ManySortedSet of I;
mode MSClosureOperator of M is reflexive monotonic idempotent MSSetOp of M;
end;

definition
let I be set ;
let M be ManySortedSet of I;
let F be ManySortedFunction of M,M;
func MSFixPoints F ->  ManySortedSubset of M means :Def12: :: CLOSURE1:def 12
 for x, i being set st i in I holds
( x in it . i iff ex f being Function st
( f = F . i &amp; x in dom f &amp; f . x = x ) );
existence
 ex b1 being ManySortedSubset of M st
for x, i being set st i in I holds
( x in b1 . i iff ex f being Function st
( f = F . i &amp; x in dom f &amp; f . x = x ) )
proofend;
uniqueness
 for b1, b2 being ManySortedSubset of M st ( for x, i being set st i in I holds
( x in b1 . i iff ex f being Function st
( f = F . i &amp; x in dom f &amp; f . x = x ) ) ) &amp; ( for x, i being set st i in I holds
( x in b2 . i iff ex f being Function st
( f = F . i &amp; x in dom f &amp; f . x = x ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines MSFixPoints CLOSURE1:def_12_:_
 for I being set
for M being ManySortedSet of I
for F being ManySortedFunction of M,M
for b4 being ManySortedSubset of M holds
( b4 = MSFixPoints F iff for x, i being set st i in I holds
( x in b4 . i iff ex f being Function st
( f = F . i &amp; x in dom f &amp; f . x = x ) ) );

registration
let I be set ;
let M be V9() ManySortedSet of I;
let F be ManySortedFunction of M,M;
cluster MSFixPoints F -> V9() ;
coherence
 MSFixPoints F is empty-yielding
proofend;
end;

theorem Th28: :: CLOSURE1:28
for I being set
for M, A being ManySortedSet of I
for F being ManySortedFunction of M,M holds
( ( A in M &amp; F .. A = A ) iff A in MSFixPoints F )
proofend;

theorem :: CLOSURE1:29
for I being set
for A being ManySortedSet of I holds MSFixPoints (id A) = A
proofend;

theorem Th30: :: CLOSURE1:30
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for J being reflexive monotonic MSSetOp of A
for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S
proofend;

theorem Th31: :: CLOSURE1:31
for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for X being Element of bool M ex SF being V8() MSSubsetFamily of M st
for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D &amp; X c= Y ) )
proofend;

theorem Th32: :: CLOSURE1:32
for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D &amp; X c= Y ) ) ) holds
for i being set
for Di being non empty set st i in I &amp; Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }
proofend;

theorem Th33: :: CLOSURE1:33
for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M ex J being MSSetOp of M st
for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D &amp; X c= Y ) ) ) holds
J .. X = meet SF
proofend;

theorem Th34: :: CLOSURE1:34
for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for A being Element of bool M
for J being MSSetOp of M st A in D &amp; ( for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D &amp; X c= Y ) ) ) holds
J .. X = meet SF ) holds
J .. A = A
proofend;

theorem :: CLOSURE1:35
for I being set
for M being ManySortedSet of I
for D being absolutely-multiplicative MSSubsetFamily of M
for A being Element of bool M
for J being MSSetOp of M st J .. A = A &amp; ( for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D &amp; X c= Y ) ) ) holds
J .. X = meet SF ) holds
A in D
proofend;

theorem Th36: :: CLOSURE1:36
for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for J being MSSetOp of M st ( for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D &amp; X c= Y ) ) ) holds
J .. X = meet SF ) holds
( J is reflexive &amp; J is monotonic )
proofend;

theorem Th37: :: CLOSURE1:37
for I being set
for M being ManySortedSet of I
for D being absolutely-multiplicative MSSubsetFamily of M
for J being MSSetOp of M st ( for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D &amp; X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent
proofend;

theorem :: CLOSURE1:38
for S being 1-sorted
for D being MSClosureSystem of S
for J being MSSetOp of the Sorts of D st ( for X being Element of bool the Sorts of D
for SF being V8() MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D &amp; X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is MSClosureOperator of the Sorts of D by Th36, Th37;

definition
let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
func ClOp->ClSys C ->  MSClosureSystem of S means :Def13: :: CLOSURE1:def 13
 ex D being MSSubsetFamily of A st
( D = MSFixPoints C &amp; it = MSClosureStr(# A,D #) );
existence
 ex b1 being MSClosureSystem of S ex D being MSSubsetFamily of A st
( D = MSFixPoints C &amp; b1 = MSClosureStr(# A,D #) )
proofend;
uniqueness
 for b1, b2 being MSClosureSystem of S st ex D being MSSubsetFamily of A st
( D = MSFixPoints C &amp; b1 = MSClosureStr(# A,D #) ) &amp; ex D being MSSubsetFamily of A st
( D = MSFixPoints C &amp; b2 = MSClosureStr(# A,D #) ) holds
b1 = b2 ;
end;

:: deftheorem Def13 defines ClOp->ClSys CLOSURE1:def_13_:_
 for S being 1-sorted
for A being ManySortedSet of the carrier of S
for C being MSClosureOperator of A
for b4 being MSClosureSystem of S holds
( b4 = ClOp->ClSys C iff ex D being MSSubsetFamily of A st
( D = MSFixPoints C &amp; b4 = MSClosureStr(# A,D #) ) );

registration
let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
cluster ClOp->ClSys C ->  strict ;
coherence
 ClOp->ClSys C is strict
proofend;
end;

registration
let S be 1-sorted ;
let A be V8() ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
cluster ClOp->ClSys C ->  non-empty ;
coherence
 ClOp->ClSys C is non-empty
proofend;
end;

definition
let S be 1-sorted ;
let D be MSClosureSystem of S;
func ClSys->ClOp D ->  MSClosureOperator of the Sorts of D means :Def14: :: CLOSURE1:def 14
 for X being Element of bool the Sorts of D
for SF being V8() MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D &amp; X c= Y ) ) ) holds
it .. X = meet SF;
existence
 ex b1 being MSClosureOperator of the Sorts of D st
for X being Element of bool the Sorts of D
for SF being V8() MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D &amp; X c= Y ) ) ) holds
b1 .. X = meet SF
proofend;
uniqueness
 for b1, b2 being MSClosureOperator of the Sorts of D st ( for X being Element of bool the Sorts of D
for SF being V8() MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D &amp; X c= Y ) ) ) holds
b1 .. X = meet SF ) &amp; ( for X being Element of bool the Sorts of D
for SF being V8() MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D &amp; X c= Y ) ) ) holds
b2 .. X = meet SF ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines ClSys->ClOp CLOSURE1:def_14_:_
 for S being 1-sorted
for D being MSClosureSystem of S
for b3 being MSClosureOperator of the Sorts of D holds
( b3 = ClSys->ClOp D iff for X being Element of bool the Sorts of D
for SF being V8() MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D &amp; X c= Y ) ) ) holds
b3 .. X = meet SF );

theorem :: CLOSURE1:39
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J
proofend;

theorem :: CLOSURE1:40
for S being 1-sorted
for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)
proofend;