:: CLOSURE1 semantic presentation

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() )
proof
assume A1: for X being ManySortedSet of F1() holds
( X in F2() iff ( X in F3() & P1[X] ) ) ; ::_thesis: F2() c= F3()
consider K being ManySortedSet of F1() such that
A2: K in F2() by PBOOLE:134;
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in F1() or F2() . i c= F3() . i )
assume A3: i in F1() ; ::_thesis: F2() . i c= F3() . i
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F2() . i or x in F3() . i )
assume A4: x in F2() . i ; ::_thesis: x in F3() . i
 dom (K +* (i .--> x)) = F1() by A3, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of F1() by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> x) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A6: X . i = (i .--> x) . i by A5, FUNCT_4:13
.= x by FUNCOP_1:72 ;
 X in F2()
proof
let s be set ; :: according to PBOOLE:def_1 ::_thesis: ( not s in F1() or X . s in F2() . s )
assume A7: s in F1() ; ::_thesis: X . s in F2() . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X . s in F2() . s
hence  X . s in F2() . s by A4, A6; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X . s in F2() . s
then  not s in dom (i .--> x) by A5, TARSKI:def_1;
then  X . s = K . s by FUNCT_4:11;
hence  X . s in F2() . s by A2, A7, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
then  X in F3() by A1;
hence  x in F3() . i by A3, A6, PBOOLE:def_1; ::_thesis: verum
end;

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  }
proof
let X be non empty set ; ::_thesis: 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  }
let x, y be set ; ::_thesis: ( x c= y implies  {  t where t is Element of X : y c= t  }  c=  {  z where z is Element of X : x c= z  }  )
assume A1: x c= y ; ::_thesis:  {  t where t is Element of X : y c= t  }  c=  {  z where z is Element of X : x c= z  }
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  t where t is Element of X : y c= t  }  or a in  {  z where z is Element of X : x c= z  }  )
assume  a in  {  t where t is Element of X : y c= t  }  ; ::_thesis: a in  {  z where z is Element of X : x c= z  }
then A2: ex b being Element of X st
( b = a & y c= b ) ;
then  x c= a by A1, XBOOLE_1:1;
hence  a in  {  z where z is Element of X : x c= z  }  by A2; ::_thesis: verum
end;

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()
proof
let I be set ; ::_thesis: for M being ManySortedSet of I st ex A being ManySortedSet of I st A in M holds
M is V8()
let M be ManySortedSet of I; ::_thesis: ( ex A being ManySortedSet of I st A in M implies M is V8() )
given A being ManySortedSet of I such that A1: A in M ; ::_thesis: M is V8()
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not M . i is empty )
assume  i in I ; ::_thesis: not M . i is empty
hence  not M . i is empty by A1, PBOOLE:def_1; ::_thesis: verum
end;

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 to PBOOLE: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
proof
let I be set ; ::_thesis: 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
let A, X be ManySortedSet of I; ::_thesis: for B being V8() ManySortedSet of I
for F being ManySortedFunction of A,B st X in A holds
F .. X in B
let B be V8() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st X in A holds
F .. X in B
let F be ManySortedFunction of A,B; ::_thesis: ( X in A implies F .. X in B )
assume A1: X in A ; ::_thesis: F .. X in B
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or (F .. X) . i in B . i )
assume A2: i in I ; ::_thesis: (F .. X) . i in B . i
reconsider g = F . i as Function ;
A3: g is Function of (A . i),(B . i) by A2, PBOOLE:def_15;
 X . i in A . i by A1, A2, PBOOLE:def_1;
then  ( dom F = I & g . (X . i) in B . i ) by A2, A3, FUNCT_2:5, PARTFUN1:def_2;
hence  (F .. X) . i in B . i by A2, PRALG_1:def_17; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: 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
let F, G be ManySortedFunction of I; ::_thesis: for A being ManySortedSet of I st A in doms G holds
F .. (G .. A) = (F ** G) .. A
A1: dom F = I by PARTFUN1:def_2;
reconsider FG = F ** G as ManySortedFunction of I by MSSUBFAM:15;
A2: dom G = I by PARTFUN1:def_2;
A3: dom FG = I by PARTFUN1:def_2;
let A be ManySortedSet of I; ::_thesis: ( A in doms G implies F .. (G .. A) = (F ** G) .. A )
assume A4: A in doms G ; ::_thesis: F .. (G .. A) = (F ** G) .. A
A5: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(F_.._(G_.._A))_._i_=_((F_**_G)_.._A)_._i
let i be set ; ::_thesis: ( i in I implies (F .. (G .. A)) . i = ((F ** G) .. A) . i )
reconsider f = F . i as Function ;
reconsider g = G . i as Function ;
reconsider fg = (F ** G) . i as Function ;
assume A6: i in I ; ::_thesis: (F .. (G .. A)) . i = ((F ** G) .. A) . i
then  dom g = (doms G) . i by MSSUBFAM:14;
then A7: A . i in dom g by A4, A6, PBOOLE:def_1;
 (G .. A) . i = g . (A . i) by A2, A6, PRALG_1:def_17;
hence (F .. (G .. A)) . i = f . (g . (A . i)) by A1, A6, PRALG_1:def_17
.= (f * g) . (A . i) by A7, FUNCT_1:13
.= fg . (A . i) by A3, A6, PBOOLE:def_19
.= ((F ** G) .. A) . i by A3, A6, PRALG_1:def_17 ;
::_thesis: verum
end;
 FG .. A is ManySortedSet of I ;
hence  F .. (G .. A) = (F ** G) .. A by A5, PBOOLE:3; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: 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
let F be ManySortedFunction of I; ::_thesis: ( F is "1-1" implies for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B )
assume A1: F is "1-1" ; ::_thesis: for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B
let A, B be ManySortedSet of I; ::_thesis: ( A in doms F & B in doms F & F .. A = F .. B implies A = B )
assume that
A2: ( A in doms F & B in doms F ) and
A3: F .. A = F .. B ; ::_thesis: A = B
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
A_._i_=_B_._i
let i be set ; ::_thesis: ( i in I implies A . i = B . i )
assume A4: i in I ; ::_thesis: A . i = B . i
reconsider f = F . i as Function ;
A5: f is one-to-one by A1, A4, MSUALG_3:1;
 dom f = (doms F) . i by A4, MSSUBFAM:14;
then A6: ( A . i in dom f & B . i in dom f ) by A2, A4, PBOOLE:def_1;
A7: dom F = I by PARTFUN1:def_2;
then f . (A . i) = (F .. A) . i by A4, PRALG_1:def_17
.= f . (B . i) by A3, A4, A7, PRALG_1:def_17 ;
hence  A . i = B . i by A5, A6, FUNCT_1:def_4; ::_thesis: verum
end;
hence  A = B by PBOOLE:3; ::_thesis: verum
end;

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"
proof
let I be set ; ::_thesis: 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"
let F be ManySortedFunction of I; ::_thesis: ( 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 ) implies F is "1-1" )
assume that
A1: doms F is V8() and
A2: for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B ; ::_thesis: F is "1-1"
consider K being ManySortedSet of I such that
A3: K in doms F by A1, PBOOLE:134;
let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds
( not i in dom F or not F . i = b1 or b1 is one-to-one )
let f be Function; ::_thesis: ( not i in dom F or not F . i = f or f is one-to-one )
assume that
A4: i in dom F and
A5: F . i = f ; ::_thesis: f is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f . x1 = f . x2 ; ::_thesis: x1 = x2
A9: dom F = I by PARTFUN1:def_2;
then  dom (K +* (i .--> x1)) = I by A4, PZFMISC1:1;
then reconsider X1 = K +* (i .--> x1) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A10: dom (i .--> x1) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A11: X1 . i = (i .--> x1) . i by A10, FUNCT_4:13
.= x1 by FUNCOP_1:72 ;
A12: X1 in doms F
proof
let s be set ; :: according to PBOOLE:def_1 ::_thesis: ( not s in I or X1 . s in (doms F) . s )
assume A13: s in I ; ::_thesis: X1 . s in (doms F) . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X1 . s in (doms F) . s
hence  X1 . s in (doms F) . s by A5, A6, A11, A13, MSSUBFAM:14; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X1 . s in (doms F) . s
then  not s in dom (i .--> x1) by A10, TARSKI:def_1;
then  X1 . s = K . s by FUNCT_4:11;
hence  X1 . s in (doms F) . s by A3, A13, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
 dom (K +* (i .--> x2)) = I by A4, A9, PZFMISC1:1;
then reconsider X2 = K +* (i .--> x2) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A14: dom (i .--> x2) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A15: X2 . i = (i .--> x2) . i by A14, FUNCT_4:13
.= x2 by FUNCOP_1:72 ;
A16: X2 in doms F
proof
let s be set ; :: according to PBOOLE:def_1 ::_thesis: ( not s in I or X2 . s in (doms F) . s )
assume A17: s in I ; ::_thesis: X2 . s in (doms F) . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X2 . s in (doms F) . s
hence  X2 . s in (doms F) . s by A5, A7, A15, A17, MSSUBFAM:14; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X2 . s in (doms F) . s
then  not s in dom (i .--> x2) by A14, TARSKI:def_1;
then  X2 . s = K . s by FUNCT_4:11;
hence  X2 . s in (doms F) . s by A3, A17, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_s_being_set_st_s_in_I_holds_
(F_.._X1)_._s_=_(F_.._X2)_._s
let s be set ; ::_thesis: ( s in I implies (F .. X1) . b1 = (F .. X2) . b1 )
assume A18: s in I ; ::_thesis: (F .. X1) . b1 = (F .. X2) . b1
percases ( s = i or s <> i ) ;
supposeA19: s = i ; ::_thesis: (F .. X1) . b1 = (F .. X2) . b1
hence (F .. X1) . s = f . (X2 . s) by A4, A5, A8, A11, A15, PRALG_1:def_17
.= (F .. X2) . s by A4, A5, A19, PRALG_1:def_17 ;
::_thesis: verum
end;
supposeA20: s <> i ; ::_thesis: (F .. X1) . b1 = (F .. X2) . b1
then  not s in dom (i .--> x2) by A14, TARSKI:def_1;
then A21: X2 . s = K . s by FUNCT_4:11;
reconsider f1 = F . s as Function ;
A22: not s in dom (i .--> x1) by A10, A20, TARSKI:def_1;
thus (F .. X1) . s = f1 . (X1 . s) by A9, A18, PRALG_1:def_17
.= f1 . (X2 . s) by A22, A21, FUNCT_4:11
.= (F .. X2) . s by A9, A18, PRALG_1:def_17 ; ::_thesis: verum
end;
end;
end;
hence  x1 = x2 by A2, A11, A15, A12, A16, PBOOLE:3; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: 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
let A, B be V8() ManySortedSet of I; ::_thesis: 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
let F, G be ManySortedFunction of A,B; ::_thesis: ( ( for M being ManySortedSet of I st M in A holds
F .. M = G .. M ) implies F = G )
assume A1: for M being ManySortedSet of I st M in A holds
F .. M = G .. M ; ::_thesis: F = G
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
F_._i_=_G_._i
let i be set ; ::_thesis: ( i in I implies F . i = G . i )
assume A2: i in I ; ::_thesis: F . i = G . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider g = G . i as Function of (A . i),(B . i) by A2, PBOOLE:def_15;
now__::_thesis:_for_x_being_set_st_x_in_A_._i_holds_
f_._x_=_g_._x
A3: dom G = I by PARTFUN1:def_2;
consider K being ManySortedSet of I such that
A4: K in A by PBOOLE:134;
let x be set ; ::_thesis: ( x in A . i implies f . x = g . x )
assume A5: x in A . i ; ::_thesis: f . x = g . x
 dom (K +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A6: dom (i .--> x) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A7: X . i = (i .--> x) . i by A6, FUNCT_4:13
.= x by FUNCOP_1:72 ;
 X in A
proof
let s be set ; :: according to PBOOLE:def_1 ::_thesis: ( not s in I or X . s in A . s )
assume A8: s in I ; ::_thesis: X . s in A . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X . s in A . s
hence  X . s in A . s by A5, A7; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X . s in A . s
then  not s in dom (i .--> x) by A6, TARSKI:def_1;
then  X . s = K . s by FUNCT_4:11;
hence  X . s in A . s by A4, A8, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
then A9: F .. X = G .. X by A1;
 dom F = I by PARTFUN1:def_2;
hence f . x = (F .. X) . i by A2, A7, PRALG_1:def_17
.= g . x by A2, A7, A9, A3, PRALG_1:def_17 ;
::_thesis: verum
end;
hence  F . i = G . i by FUNCT_2:12; ::_thesis: verum
end;
hence  F = G by PBOOLE:3; ::_thesis: verum
end;

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() )
proof
 [[0]] I c= M by MBOOLEAN:5;
then  [[0]] I in bool M by MBOOLEAN:1;
then reconsider a = [[0]] I as Element of bool M by MSSUBFAM:11;
take  a ; ::_thesis: ( a is V9() & a is V42() )
thus  ( a is V9() & a is V42() ) ; ::_thesis: verum
end;
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
proof
let I be set ; ::_thesis: for M being V8() ManySortedSet of I
for X being Element of M holds X = (id M) .. X
let M be V8() ManySortedSet of I; ::_thesis: for X being Element of M holds X = (id M) .. X
let X be Element of M; ::_thesis: X = (id M) .. X
set F = id M;
A1: dom (id M) = I by PARTFUN1:def_2;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_((id_M)_.._X)_._i
let i be set ; ::_thesis: ( i in I implies X . i = ((id M) .. X) . i )
reconsider g = (id M) . i as Function ;
assume A2: i in I ; ::_thesis: X . i = ((id M) .. X) . i
then  ( X . i is Element of M . i & (id M) . i = id (M . i) ) by MSUALG_3:def_1, PBOOLE:def_14;
then  g . (X . i) = X . i by A2, FUNCT_1:18;
hence  X . i = ((id M) .. X) . i by A1, A2, PRALG_1:def_17; ::_thesis: verum
end;
hence  X = (id M) .. X by PBOOLE:3; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: 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
let M be V8() ManySortedSet of I; ::_thesis: for X, Y being Element of M st X c= Y holds
(id M) .. X c= (id M) .. Y
let X, Y be Element of M; ::_thesis: ( X c= Y implies (id M) .. X c= (id M) .. Y )
assume A1: X c= Y ; ::_thesis: (id M) .. X c= (id M) .. Y
 (id M) .. X = X by Th8;
hence  (id M) .. X c= (id M) .. Y by A1, Th8; ::_thesis: verum
end;

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)
proof
let I be set ; ::_thesis: 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)
let M be V8() ManySortedSet of I; ::_thesis: 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)
let X, Y be Element of M; ::_thesis: ( X \/ Y is Element of M implies (id M) .. (X \/ Y) = ((id M) .. X) \/ ((id M) .. Y) )
set F = id M;
assume  X \/ Y is Element of M ; ::_thesis: (id M) .. (X \/ Y) = ((id M) .. X) \/ ((id M) .. Y)
hence (id M) .. (X \/ Y) = X \/ Y by Th8
.= ((id M) .. X) \/ Y by Th8
.= ((id M) .. X) \/ ((id M) .. Y) by Th8 ;
::_thesis: verum
end;

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 )
proof
let I be set ; ::_thesis: 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 )
let M be ManySortedSet of I; ::_thesis: 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 )
let X be Element of bool M; ::_thesis: 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 )
let i, x be set ; ::_thesis: ( i in I & x in ((id (bool M)) .. X) . i implies ex Y being V42() Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i ) )
assume that
A1: i in I and
A2: x in ((id (bool M)) .. X) . i ; ::_thesis: ex Y being V42() Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
A3: x in X . i by A2, Th8;
set Y = (I --> {}) +* (i .--> {x});
 dom ((I --> {}) +* (i .--> {x})) = I by A1, PZFMISC1:1;
then reconsider Y = (I --> {}) +* (i .--> {x}) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A4: dom (i .--> {x}) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A5: Y . i = (i .--> {x}) . i by A4, FUNCT_4:13
.= {x} by FUNCOP_1:72 ;
 X in bool M by MSSUBFAM:12;
then  X c= M by MBOOLEAN:18;
then A6: X . i c= M . i by A1, PBOOLE:def_2;
 Y is Element of bool M
proof
let j be set ; :: according to PBOOLE:def_14 ::_thesis: ( not j in I or Y . j is Element of (bool M) . j )
assume A7: j in I ; ::_thesis: Y . j is Element of (bool M) . j
now__::_thesis:_(_(_j_=_i_&_Y_._j_is_Element_of_(bool_M)_._j_)_or_(_j_<>_i_&_Y_._j_is_Element_of_(bool_M)_._j_)_)
percases ( j = i or j <> i ) ;
caseA8: j = i ; ::_thesis: Y . j is Element of (bool M) . j
then  {x} c= M . j by A3, A6, ZFMISC_1:31;
hence  Y . j is Element of (bool M) . j by A5, A7, A8, MBOOLEAN:def_1; ::_thesis: verum
end;
case j <> i ; ::_thesis: Y . j is Element of (bool M) . j
then  not j in dom (i .--> {x}) by A4, TARSKI:def_1;
then  Y . j = (I --> {}) . j by FUNCT_4:11;
then  Y . j = {} by A7, FUNCOP_1:7;
then  Y . j c= M . j by XBOOLE_1:2;
hence  Y . j is Element of (bool M) . j by A7, MBOOLEAN:def_1; ::_thesis: verum
end;
end;
end;
hence  Y . j is Element of (bool M) . j ; ::_thesis: verum
end;
then reconsider Y = Y as Element of bool M ;
 Y is V42()
proof
let j be set ; :: according to FINSET_1:def_5 ::_thesis: ( not j in I or Y . j is finite )
assume A9: j in I ; ::_thesis: Y . j is finite
now__::_thesis:_(_(_j_=_i_&_Y_._j_is_finite_)_or_(_j_<>_i_&_Y_._j_is_finite_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: Y . j is finite
hence  Y . j is finite by A5; ::_thesis: verum
end;
case j <> i ; ::_thesis: Y . j is finite
then  not j in dom (i .--> {x}) by A4, TARSKI:def_1;
then  Y . j = (I --> {}) . j by FUNCT_4:11;
hence  Y . j is finite by A9, FUNCOP_1:7; ::_thesis: verum
end;
end;
end;
hence  Y . j is finite ; ::_thesis: verum
end;
then reconsider Y = Y as V42() Element of bool M ;
take  Y ; ::_thesis: ( Y c= X & x in ((id (bool M)) .. Y) . i )
thus  Y c= X ::_thesis: x in ((id (bool M)) .. Y) . i
proof
let j be set ; :: according to PBOOLE:def_2 ::_thesis: ( not j in I or Y . j c= X . j )
assume A10: j in I ; ::_thesis: Y . j c= X . j
now__::_thesis:_(_(_j_=_i_&_Y_._j_c=_X_._j_)_or_(_j_<>_i_&_Y_._j_c=_X_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: Y . j c= X . j
hence  Y . j c= X . j by A3, A5, ZFMISC_1:31; ::_thesis: verum
end;
case j <> i ; ::_thesis: Y . j c= X . j
then  not j in dom (i .--> {x}) by A4, TARSKI:def_1;
then  Y . j = (I --> {}) . j by FUNCT_4:11;
then  Y . j = {} by A10, FUNCOP_1:7;
hence  Y . j c= X . j by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
hence  Y . j c= X . j ; ::_thesis: verum
end;
 x in Y . i by A5, TARSKI:def_1;
hence  x in ((id (bool M)) .. Y) . i by Th8; ::_thesis: verum
end;

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 )
proof
reconsider F = id (bool M) as MSSetOp of M ;
take  F ; ::_thesis: ( F is reflexive & F is monotonic & F is idempotent & F is topological )
thus  F is reflexive ::_thesis: ( F is monotonic & F is idempotent & F is topological )
proof
let X be Element of bool M; :: according to CLOSURE1:def_1 ::_thesis: X c= F .. X
thus  X c= F .. X by Th8; ::_thesis: verum
end;
thus  F is monotonic ::_thesis: ( F is idempotent & F is topological )
proof
let X, Y be Element of bool M; :: according to CLOSURE1:def_2 ::_thesis: ( X c= Y implies F .. X c= F .. Y )
assume  X c= Y ; ::_thesis: F .. X c= F .. Y
hence  F .. X c= F .. Y by Th9; ::_thesis: verum
end;
thus  F is idempotent ::_thesis: F is topological
proof
let X be Element of bool M; :: according to CLOSURE1:def_3 ::_thesis: F .. X = F .. (F .. X)
thus  F .. X = F .. (F .. X) by Th8; ::_thesis: verum
end;
thus  F is topological ::_thesis: verum
proof
let X, Y be Element of bool M; :: according to CLOSURE1:def_4 ::_thesis: F .. (X \/ Y) = (F .. X) \/ (F .. Y)
 Y in bool M by MSSUBFAM:12;
then A1: Y c= M by MBOOLEAN:1;
 X in bool M by MSSUBFAM:12;
then  X c= M by MBOOLEAN:1;
then  X \/ Y c= M by A1, PBOOLE:16;
then  X \/ Y in bool M by MBOOLEAN:1;
then  X \/ Y is Element of bool M by MSSUBFAM:11;
hence  F .. (X \/ Y) = (F .. X) \/ (F .. Y) by Th10; ::_thesis: verum
end;
end;
end;

theorem :: CLOSURE1:12
for I being set
for A being ManySortedSet of I holds id (bool A) is reflexive MSSetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (bool A) is reflexive MSSetOp of A
let A be ManySortedSet of I; ::_thesis: id (bool A) is reflexive MSSetOp of A
reconsider a = id (bool A) as MSSetOp of A ;
 a is reflexive
proof
let b be Element of bool A; :: according to CLOSURE1:def_1 ::_thesis: b c= a .. b
thus  b c= a .. b by Th8; ::_thesis: verum
end;
hence  id (bool A) is reflexive MSSetOp of A ; ::_thesis: verum
end;

theorem :: CLOSURE1:13
for I being set
for A being ManySortedSet of I holds id (bool A) is monotonic MSSetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (bool A) is monotonic MSSetOp of A
let A be ManySortedSet of I; ::_thesis: id (bool A) is monotonic MSSetOp of A
reconsider a = id (bool A) as MSSetOp of A ;
 a is monotonic
proof
let X, Y be Element of bool A; :: according to CLOSURE1:def_2 ::_thesis: ( X c= Y implies a .. X c= a .. Y )
assume  X c= Y ; ::_thesis: a .. X c= a .. Y
hence  a .. X c= a .. Y by Th9; ::_thesis: verum
end;
hence  id (bool A) is monotonic MSSetOp of A ; ::_thesis: verum
end;

theorem :: CLOSURE1:14
for I being set
for A being ManySortedSet of I holds id (bool A) is idempotent MSSetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (bool A) is idempotent MSSetOp of A
let A be ManySortedSet of I; ::_thesis: id (bool A) is idempotent MSSetOp of A
reconsider a = id (bool A) as MSSetOp of A ;
 a is idempotent
proof
let X be Element of bool A; :: according to CLOSURE1:def_3 ::_thesis: a .. X = a .. (a .. X)
thus  a .. X = a .. (a .. X) by Th8; ::_thesis: verum
end;
hence  id (bool A) is idempotent MSSetOp of A ; ::_thesis: verum
end;

theorem :: CLOSURE1:15
for I being set
for A being ManySortedSet of I holds id (bool A) is topological MSSetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (bool A) is topological MSSetOp of A
let A be ManySortedSet of I; ::_thesis: id (bool A) is topological MSSetOp of A
reconsider a = id (bool A) as MSSetOp of A ;
 a is topological
proof
let X, Y be Element of bool A; :: according to CLOSURE1:def_4 ::_thesis: a .. (X \/ Y) = (a .. X) \/ (a .. Y)
 Y in bool A by MSSUBFAM:12;
then A1: Y c= A by MBOOLEAN:1;
 X in bool A by MSSUBFAM:12;
then  X c= A by MBOOLEAN:1;
then  X \/ Y c= A by A1, PBOOLE:16;
then  X \/ Y in bool A by MBOOLEAN:1;
then  X \/ Y is Element of bool A by MSSUBFAM:11;
hence  a .. (X \/ Y) = (a .. X) \/ (a .. Y) by Th10; ::_thesis: verum
end;
hence  id (bool A) is topological MSSetOp of A ; ::_thesis: verum
end;


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
proof
let I be set ; ::_thesis: 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
let M be ManySortedSet of I; ::_thesis: for P being MSSetOp of M
for E being Element of bool M st E = M & P is reflexive holds
E = P .. E
let P be MSSetOp of M; ::_thesis: for E being Element of bool M st E = M & P is reflexive holds
E = P .. E
let E be Element of bool M; ::_thesis: ( E = M & P is reflexive implies E = P .. E )
assume A1: E = M ; ::_thesis: ( not P is reflexive or E = P .. E )
assume  P is reflexive ; ::_thesis: E = P .. E
then A2: E c= P .. E by Def1;
 P .. E in bool E by A1, MSSUBFAM:12;
then  P .. E c= E by MBOOLEAN:18;
hence  E = P .. E by A2, PBOOLE:146; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: 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
let M be ManySortedSet of I; ::_thesis: 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
let P be MSSetOp of M; ::_thesis: ( P is reflexive & ( for X being Element of bool M holds P .. X c= X ) implies P is idempotent )
assume that
A1: P is reflexive and
A2: for X being Element of bool M holds P .. X c= X ; ::_thesis: P is idempotent
let X be Element of bool M; :: according to CLOSURE1:def_3 ::_thesis: P .. X = P .. (P .. X)
A3: P .. X c= P .. (P .. X) by A1, Def1;
 P .. (P .. X) c= P .. X by A2;
hence  P .. X = P .. (P .. X) by A3, PBOOLE:146; ::_thesis: verum
end;

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)
proof
let I be set ; ::_thesis: 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)
let M be ManySortedSet of I; ::_thesis: 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)
let P be MSSetOp of M; ::_thesis: for E, T being Element of bool M st P is monotonic holds
P .. (E /\ T) c= (P .. E) /\ (P .. T)
let E, T be Element of bool M; ::_thesis: ( P is monotonic implies P .. (E /\ T) c= (P .. E) /\ (P .. T) )
assume A1: P is monotonic ; ::_thesis: P .. (E /\ T) c= (P .. E) /\ (P .. T)
 E in bool M by MSSUBFAM:12;
then  E c= M by MBOOLEAN:1;
then  E /\ T c= M by MBOOLEAN:14;
then  E /\ T in bool M by MBOOLEAN:1;
then A2: E /\ T is Element of bool M by MSSUBFAM:11;
 E /\ T c= T by PBOOLE:15;
then A3: P .. (E /\ T) c= P .. T by A1, A2, Def2;
 E /\ T c= E by PBOOLE:15;
then  P .. (E /\ T) c= P .. E by A1, A2, Def2;
hence  P .. (E /\ T) c= (P .. E) /\ (P .. T) by A3, PBOOLE:17; ::_thesis: verum
end;

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
proof
let P be MSSetOp of M; ::_thesis: ( P is topological implies P is monotonic )
assume A1: P is topological ; ::_thesis: P is monotonic
let X, Y be Element of bool M; :: according to CLOSURE1:def_2 ::_thesis: ( X c= Y implies P .. X c= P .. Y )
assume A2: X c= Y ; ::_thesis: P .. X c= P .. Y
(P .. X) \/ (P .. Y) = P .. (X \/ Y) by A1, Def4
.= P .. Y by A2, PBOOLE:22 ;
hence  P .. X c= P .. Y by PBOOLE:26; ::_thesis: verum
end;
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)
proof
let I be set ; ::_thesis: 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)
let M be ManySortedSet of I; ::_thesis: 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)
let P be MSSetOp of M; ::_thesis: for E, T being Element of bool M st P is topological holds
(P .. E) \ (P .. T) c= P .. (E \ T)
let E, T be Element of bool M; ::_thesis: ( P is topological implies (P .. E) \ (P .. T) c= P .. (E \ T) )
 E in bool M by MSSUBFAM:12;
then  E c= M by MBOOLEAN:1;
then  E \ T c= M by MBOOLEAN:15;
then  E \ T in bool M by MBOOLEAN:1;
then A1: E \ T is Element of bool M by MSSUBFAM:11;
assume A2: P is topological ; ::_thesis: (P .. E) \ (P .. T) c= P .. (E \ T)
then (P .. E) \/ (P .. T) = P .. (E \/ T) by Def4
.= P .. ((E \ T) \/ T) by PBOOLE:67
.= (P .. (E \ T)) \/ (P .. T) by A1, A2, Def4 ;
then  P .. E c= (P .. (E \ T)) \/ (P .. T) by PBOOLE:14;
then  (P .. E) \ (P .. T) c= ((P .. (E \ T)) \/ (P .. T)) \ (P .. T) by PBOOLE:53;
then A3: (P .. E) \ (P .. T) c= (P .. (E \ T)) \ (P .. T) by PBOOLE:75;
 (P .. (E \ T)) \ (P .. T) c= P .. (E \ T) by PBOOLE:56;
hence  (P .. E) \ (P .. T) c= P .. (E \ T) by A3, PBOOLE:13; ::_thesis: verum
end;

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
proof
 P ** R is ManySortedFunction of bool M, bool M ;
hence  P ** R is MSSetOp of M ; ::_thesis: verum
end;
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
proof
let I be set ; ::_thesis: 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
let M be ManySortedSet of I; ::_thesis: for P, R being MSSetOp of M st P is reflexive & R is reflexive holds
P ** R is reflexive
let P, R be MSSetOp of M; ::_thesis: ( P is reflexive & R is reflexive implies P ** R is reflexive )
assume A1: ( P is reflexive & R is reflexive ) ; ::_thesis: P ** R is reflexive
let X be Element of bool M; :: according to CLOSURE1:def_1 ::_thesis: X c= (P ** R) .. X
 ( X c= R .. X & R .. X c= P .. (R .. X) ) by A1, Def1;
then  ( doms R = bool M & X c= P .. (R .. X) ) by MSSUBFAM:17, PBOOLE:13;
hence  X c= (P ** R) .. X by Th4, MSSUBFAM:12; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: 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
let M be ManySortedSet of I; ::_thesis: for P, R being MSSetOp of M st P is monotonic & R is monotonic holds
P ** R is monotonic
let P, R be MSSetOp of M; ::_thesis: ( P is monotonic & R is monotonic implies P ** R is monotonic )
assume that
A1: P is monotonic and
A2: R is monotonic ; ::_thesis: P ** R is monotonic
A3: doms R = bool M by MSSUBFAM:17;
let X, Y be Element of bool M; :: according to CLOSURE1:def_2 ::_thesis: ( X c= Y implies (P ** R) .. X c= (P ** R) .. Y )
assume  X c= Y ; ::_thesis: (P ** R) .. X c= (P ** R) .. Y
then  R .. X c= R .. Y by A2, Def2;
then  P .. (R .. X) c= P .. (R .. Y) by A1, Def2;
then  P .. (R .. X) c= (P ** R) .. Y by A3, Th4, MSSUBFAM:12;
hence  (P ** R) .. X c= (P ** R) .. Y by A3, Th4, MSSUBFAM:12; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: 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
let M be ManySortedSet of I; ::_thesis: for P, R being MSSetOp of M st P is idempotent & R is idempotent & P ** R = R ** P holds
P ** R is idempotent
let P, R be MSSetOp of M; ::_thesis: ( P is idempotent & R is idempotent & P ** R = R ** P implies P ** R is idempotent )
assume that
A1: P is idempotent and
A2: R is idempotent and
A3: P ** R = R ** P ; ::_thesis: P ** R is idempotent
let X be Element of bool M; :: according to CLOSURE1:def_3 ::_thesis: (P ** R) .. X = (P ** R) .. ((P ** R) .. X)
A4: doms P = bool M by MSSUBFAM:17;
A5: doms R = bool M by MSSUBFAM:17;
hence (P ** R) .. X = P .. (R .. X) by Th4, MSSUBFAM:12
.= P .. (R .. (R .. X)) by A2, Def3
.= P .. (P .. (R .. (R .. X))) by A1, Def3
.= P .. ((R ** P) .. (R .. X)) by A3, A5, Th4, MSSUBFAM:12
.= P .. (R .. (P .. (R .. X))) by A4, Th4, MSSUBFAM:12
.= P .. (R .. ((P ** R) .. X)) by A5, Th4, MSSUBFAM:12
.= (P ** R) .. ((P ** R) .. X) by A5, Th4, MSSUBFAM:12 ;
::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: 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
let M be ManySortedSet of I; ::_thesis: for P, R being MSSetOp of M st P is topological & R is topological holds
P ** R is topological
let P, R be MSSetOp of M; ::_thesis: ( P is topological & R is topological implies P ** R is topological )
assume that
A1: P is topological and
A2: R is topological ; ::_thesis: P ** R is topological
let X, Y be Element of bool M; :: according to CLOSURE1:def_4 ::_thesis: (P ** R) .. (X \/ Y) = ((P ** R) .. X) \/ ((P ** R) .. Y)
A3: doms R = bool M by MSSUBFAM:17;
 Y in bool M by MSSUBFAM:12;
then A4: Y c= M by MBOOLEAN:1;
 X in bool M by MSSUBFAM:12;
then  X c= M by MBOOLEAN:1;
then  X \/ Y c= M by A4, PBOOLE:16;
then  X \/ Y in doms R by A3, MBOOLEAN:1;
hence (P ** R) .. (X \/ Y) = P .. (R .. (X \/ Y)) by Th4
.= P .. ((R .. X) \/ (R .. Y)) by A2, Def4
.= (P .. (R .. X)) \/ (P .. (R .. Y)) by A1, Def4
.= ((P ** R) .. X) \/ (P .. (R .. Y)) by A3, Th4, MSSUBFAM:12
.= ((P ** R) .. X) \/ ((P ** R) .. Y) by A3, Th4, MSSUBFAM:12 ;
::_thesis: verum
end;

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 to PBOOLE: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_&_a_._j_in_(bool_M)_._j_)_or_(_j_<>_i_&_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 & i in I & f = P . i holds
for x being Element of bool (M . i) holds x c= f . x
proof
let i, I be set ; ::_thesis: for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds
for x being Element of bool (M . i) holds x c= f . x
let M be ManySortedSet of I; ::_thesis: for f being Function
for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds
for x being Element of bool (M . i) holds x c= f . x
let f be Function; ::_thesis: for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds
for x being Element of bool (M . i) holds x c= f . x
let P be MSSetOp of M; ::_thesis: ( P is reflexive & i in I & f = P . i implies for x being Element of bool (M . i) holds x c= f . x )
assume that
A1: P is reflexive and
A2: i in I and
A3: f = P . i ; ::_thesis: for x being Element of bool (M . i) holds x c= f . x
let x be Element of bool (M . i); ::_thesis: x c= f . x
 dom (([[0]] I) +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = ([[0]] I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
 X is Element of bool M by Lm2, MSSUBFAM:11;
then  X c= P .. X by A1, Def1;
then A4: X . i c= (P .. X) . i by A2, PBOOLE:def_2;
 ( dom (i .--> x) = {i} & i in {i} ) by FUNCOP_1:13, TARSKI:def_1;
then A5: X . i = (i .--> x) . i by FUNCT_4:13
.= x by FUNCOP_1:72 ;
 i in dom P by A2, PARTFUN1:def_2;
hence  x c= f . x by A3, A5, A4, PRALG_1:def_17; ::_thesis: verum
end;

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 & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
proof
let i, I be set ; ::_thesis: for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let M be ManySortedSet of I; ::_thesis: for f being Function
for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let f be Function; ::_thesis: for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let P be MSSetOp of M; ::_thesis: ( P is monotonic & i in I & f = P . i implies for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y )
assume that
A1: P is monotonic and
A2: i in I and
A3: f = P . i ; ::_thesis: for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y
let x, y be Element of bool (M . i); ::_thesis: ( x c= y implies f . x c= f . y )
assume A4: x c= y ; ::_thesis: f . x c= f . y
 dom (([[0]] I) +* (i .--> y)) = I by A2, PZFMISC1:1;
then reconsider Y = ([[0]] I) +* (i .--> y) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
 dom (([[0]] I) +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = ([[0]] I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: i in {i} by TARSKI:def_1;
A6: dom (i .--> y) = {i} by FUNCOP_1:13;
then A7: Y . i = (i .--> y) . i by A5, FUNCT_4:13
.= y by FUNCOP_1:72 ;
A8: dom (i .--> x) = {i} by FUNCOP_1:13;
then A9: X . i = (i .--> x) . i by A5, FUNCT_4:13
.= x by FUNCOP_1:72 ;
A10: X c= Y
proof
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in I or X . s c= Y . s )
assume  s in I ; ::_thesis: X . s c= Y . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X . s c= Y . s
hence  X . s c= Y . s by A4, A9, A7; ::_thesis: verum
end;
supposeA11: s <> i ; ::_thesis: X . s c= Y . s
then  not s in dom (i .--> x) by A8, TARSKI:def_1;
then A12: X . s = ([[0]] I) . s by FUNCT_4:11;
 not s in dom (i .--> y) by A6, A11, TARSKI:def_1;
hence  X . s c= Y . s by A12, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
A13: i in dom P by A2, PARTFUN1:def_2;
 ( X is Element of bool M & Y is Element of bool M ) by Lm2, MSSUBFAM:11;
then  P .. X c= P .. Y by A1, A10, Def2;
then  (P .. X) . i c= (P .. Y) . i by A2, PBOOLE:def_2;
then  f . (X . i) c= (P .. Y) . i by A3, A13, PRALG_1:def_17;
hence  f . x c= f . y by A3, A9, A7, A13, PRALG_1:def_17; ::_thesis: verum
end;

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 & i in I & f = P . i holds
for x being Element of bool (M . i) holds f . x = f . (f . x)
proof
let i, I be set ; ::_thesis: for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds
for x being Element of bool (M . i) holds f . x = f . (f . x)
let M be ManySortedSet of I; ::_thesis: for f being Function
for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds
for x being Element of bool (M . i) holds f . x = f . (f . x)
let f be Function; ::_thesis: for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds
for x being Element of bool (M . i) holds f . x = f . (f . x)
let P be MSSetOp of M; ::_thesis: ( P is idempotent & i in I & f = P . i implies for x being Element of bool (M . i) holds f . x = f . (f . x) )
assume that
A1: P is idempotent and
A2: i in I and
A3: f = P . i ; ::_thesis: for x being Element of bool (M . i) holds f . x = f . (f . x)
A4: i in dom P by A2, PARTFUN1:def_2;
let x be Element of bool (M . i); ::_thesis: f . x = f . (f . x)
 dom (([[0]] I) +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = ([[0]] I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: X is Element of bool M by Lm2, MSSUBFAM:11;
 ( dom (i .--> x) = {i} & i in {i} ) by FUNCOP_1:13, TARSKI:def_1;
then A6: X . i = (i .--> x) . i by FUNCT_4:13
.= x by FUNCOP_1:72 ;
hence f . x = (P .. X) . i by A3, A4, PRALG_1:def_17
.= (P .. (P .. X)) . i by A1, A5, Def3
.= f . ((P .. X) . i) by A3, A4, PRALG_1:def_17
.= f . (f . x) by A3, A6, A4, PRALG_1:def_17 ;
::_thesis: verum
end;

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 & i in I & f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
proof
let i, I be set ; ::_thesis: for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is topological & i in I & f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
let M be ManySortedSet of I; ::_thesis: for f being Function
for P being MSSetOp of M st P is topological & i in I & f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
let f be Function; ::_thesis: for P being MSSetOp of M st P is topological & i in I & f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
let P be MSSetOp of M; ::_thesis: ( P is topological & i in I & f = P . i implies for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y) )
assume that
A1: P is topological and
A2: i in I and
A3: f = P . i ; ::_thesis: for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
A4: i in dom P by A2, PARTFUN1:def_2;
let x, y be Element of bool (M . i); ::_thesis: f . (x \/ y) = (f . x) \/ (f . y)
 dom (([[0]] I) +* (i .--> y)) = I by A2, PZFMISC1:1;
then reconsider Y = ([[0]] I) +* (i .--> y) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
 dom (([[0]] I) +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = ([[0]] I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: i in {i} by TARSKI:def_1;
 dom (i .--> y) = {i} by FUNCOP_1:13;
then A6: Y . i = (i .--> y) . i by A5, FUNCT_4:13
.= y by FUNCOP_1:72 ;
A7: ( X is Element of bool M & Y is Element of bool M ) by Lm2, MSSUBFAM:11;
 dom (i .--> x) = {i} by FUNCOP_1:13;
then A8: X . i = (i .--> x) . i by A5, FUNCT_4:13
.= x by FUNCOP_1:72 ;
hence f . (x \/ y) = f . ((X \/ Y) . i) by A2, A6, PBOOLE:def_4
.= (P .. (X \/ Y)) . i by A3, A4, PRALG_1:def_17
.= ((P .. X) \/ (P .. Y)) . i by A1, A7, Def4
.= ((P .. X) . i) \/ ((P .. Y) . i) by A2, PBOOLE:def_4
.= (f . (X . i)) \/ ((P .. Y) . i) by A3, A4, PRALG_1:def_17
.= (f . x) \/ (f . y) by A3, A8, A6, A4, PRALG_1:def_17 ;
::_thesis: verum
end;

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 & MSFull MS is additive & MSFull MS is absolutely-additive & MSFull MS is multiplicative & MSFull MS is absolutely-multiplicative & MSFull MS is properly-upper-bound & MSFull MS is properly-lower-bound )
proof
thus  MSFull MS is strict ; ::_thesis: ( MSFull MS is additive & MSFull MS is absolutely-additive & MSFull MS is multiplicative & MSFull MS is absolutely-multiplicative & MSFull MS is properly-upper-bound & MSFull MS is properly-lower-bound )
thus  ( the Family of (MSFull MS) is additive & the Family of (MSFull MS) is absolutely-additive & the Family of (MSFull MS) is multiplicative & the Family of (MSFull MS) is absolutely-multiplicative & the Family of (MSFull MS) is properly-upper-bound & the Family of (MSFull MS) is properly-lower-bound ) ; :: according to CLOSURE1:def_5,CLOSURE1:def_6,CLOSURE1:def_7,CLOSURE1:def_8,CLOSURE1:def_9,CLOSURE1:def_10 ::_thesis: verum
end;
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 & b1 is non-empty & b1 is additive & b1 is absolutely-additive & b1 is multiplicative & b1 is absolutely-multiplicative & b1 is properly-upper-bound & b1 is properly-lower-bound )
proof
set a = the non-empty many-sorted over S;
take  MSFull the non-empty many-sorted over S ; ::_thesis: ( MSFull the non-empty many-sorted over S is strict & MSFull the non-empty many-sorted over S is non-empty & MSFull the non-empty many-sorted over S is additive & MSFull the non-empty many-sorted over S is absolutely-additive & MSFull the non-empty many-sorted over S is multiplicative & MSFull the non-empty many-sorted over S is absolutely-multiplicative & MSFull the non-empty many-sorted over S is properly-upper-bound & MSFull the non-empty many-sorted over S is properly-lower-bound )
thus  ( MSFull the non-empty many-sorted over S is strict & MSFull the non-empty many-sorted over S is non-empty & MSFull the non-empty many-sorted over S is additive & MSFull the non-empty many-sorted over S is absolutely-additive & MSFull the non-empty many-sorted over S is multiplicative & MSFull the non-empty many-sorted over S is absolutely-multiplicative & MSFull the non-empty many-sorted over S is properly-upper-bound & MSFull the non-empty many-sorted over S is properly-lower-bound ) ; ::_thesis: verum
end;
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
proof
thus  the Sorts of MSClosureStr(# M,F #) is V8() ; :: according to MSUALG_1:def_3 ::_thesis: verum
end;
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
proof
let CS be MSClosureStr over S; ::_thesis: ( CS is absolutely-additive implies CS is additive )
assume  CS is absolutely-additive ; ::_thesis: CS is additive
hence  the Family of CS is additive ; :: according to CLOSURE1:def_5 ::_thesis: verum
end;
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
proof
let CS be MSClosureStr over S; ::_thesis: ( CS is absolutely-multiplicative implies CS is multiplicative )
assume  CS is absolutely-multiplicative ; ::_thesis: CS is multiplicative
hence  the Family of CS is multiplicative ; :: according to CLOSURE1:def_7 ::_thesis: verum
end;
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
proof
let CS be MSClosureStr over S; ::_thesis: ( CS is absolutely-multiplicative implies CS is properly-upper-bound )
assume  CS is absolutely-multiplicative ; ::_thesis: CS is properly-upper-bound
hence  the Family of CS is properly-upper-bound ; :: according to CLOSURE1:def_9 ::_thesis: verum
end;
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
proof
let CS be MSClosureStr over S; ::_thesis: ( CS is absolutely-additive implies CS is properly-lower-bound )
assume  CS is absolutely-additive ; ::_thesis: CS is properly-lower-bound
hence  the Family of CS is properly-lower-bound ; :: according to CLOSURE1:def_10 ::_thesis: verum
end;
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 & x in dom f & 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 & x in dom f & f . x = x ) )
proof
defpred S1[ set , set ] means  for x being set holds
( x in $2 iff ( x in M . $1 & ex f being Function st
( f = F . $1 & x in dom f & f . x = x ) ) );
A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
ex_j_being_set_st_S1[i,j]
let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] )
assume  i in I ; ::_thesis: ex j being set st S1[i,j]
defpred S2[ set ] means  ex f being Function st
( f = F . i & $1 in dom f & f . $1 = $1 );
consider j being set  such that
A2: for x being set holds
( x in j iff ( x in M . i & S2[x] ) ) from XBOOLE_0:sch_1();
take j = j; ::_thesis: S1[i,j]
thus  S1[i,j] by A2; ::_thesis: verum
end;
consider A being ManySortedSet of I such that
A3: for i being set st i in I holds
S1[i,A . i] from PBOOLE:sch_3(A1);
 A is ManySortedSubset of M
proof
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or A . i c= M . i )
assume A4: i in I ; ::_thesis: A . i c= M . i
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in M . i )
assume  x in A . i ; ::_thesis: x in M . i
hence  x in M . i by A3, A4; ::_thesis: verum
end;
then reconsider A = A as ManySortedSubset of M ;
take  A ; ::_thesis: for x, i being set st i in I holds
( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) )
thus  for x, i being set st i in I holds
( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) ::_thesis: verum
proof
let x, i be set ; ::_thesis: ( i in I implies ( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) )
assume A5: i in I ; ::_thesis: ( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) )
hence  ( x in A . i implies ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) by A3; ::_thesis: ( ex f being Function st
( f = F . i & x in dom f & f . x = x ) implies x in A . i )
given f being Function such that A6: f = F . i and
A7: ( x in dom f & f . x = x ) ; ::_thesis: x in A . i
 doms F = M by MSSUBFAM:17;
then  dom f = M . i by A5, A6, MSSUBFAM:14;
hence  x in A . i by A3, A5, A6, A7; ::_thesis: verum
end;
end;
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 & x in dom f & f . x = x ) ) ) & ( for x, i being set st i in I holds
( x in b2 . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) ) holds
b1 = b2
proof
let A, B be ManySortedSubset of M; ::_thesis: ( ( for x, i being set st i in I holds
( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) ) & ( for x, i being set st i in I holds
( x in B . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) ) implies A = B )
assume that
A8: for x, i being set st i in I holds
( x in A . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) and
A9: for x, i being set st i in I holds
( x in B . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) ; ::_thesis: A = B
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
A_._i_=_B_._i
let i be set ; ::_thesis: ( i in I implies A . i = B . i )
assume A10: i in I ; ::_thesis: A . i = B . i
thus  A . i = B . i ::_thesis: verum
proof
thus  A . i c= B . i :: according to XBOOLE_0:def_10 ::_thesis: B . i c= A . i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in B . i )
assume  x in A . i ; ::_thesis: x in B . i
then  ex f being Function st
( f = F . i & x in dom f & f . x = x ) by A8, A10;
hence  x in B . i by A9, A10; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B . i or x in A . i )
assume  x in B . i ; ::_thesis: x in A . i
then  ex f being Function st
( f = F . i & x in dom f & f . x = x ) by A9, A10;
hence  x in A . i by A8, A10; ::_thesis: verum
end;
end;
hence  A = B by PBOOLE:3; ::_thesis: verum
end;
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 & x in dom f & 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
proof
let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( not i in I or (MSFixPoints F) . i is empty )
assume A1: i in I ; ::_thesis: (MSFixPoints F) . i is empty
assume  not (MSFixPoints F) . i is empty ; ::_thesis: contradiction
then consider x being set  such that
A2: x in (MSFixPoints F) . i by XBOOLE_0:def_1;
consider f being Function such that
A3: f = F . i and
A4: x in dom f and
 f . x = x by A1, A2, Def12;
 M . i = {} ;
then  f is Function of {},{} by A1, A3, PBOOLE:def_15;
hence  contradiction by A4; ::_thesis: verum
end;
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 & F .. A = A ) iff A in MSFixPoints F )
proof
let I be set ; ::_thesis: for M, A being ManySortedSet of I
for F being ManySortedFunction of M,M holds
( ( A in M & F .. A = A ) iff A in MSFixPoints F )
let M, A be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of M,M holds
( ( A in M & F .. A = A ) iff A in MSFixPoints F )
let F be ManySortedFunction of M,M; ::_thesis: ( ( A in M & F .. A = A ) iff A in MSFixPoints F )
thus  ( A in M & F .. A = A implies A in MSFixPoints F ) ::_thesis: ( A in MSFixPoints F implies ( A in M & F .. A = A ) )
proof
assume that
A1: A in M and
A2: F .. A = A ; ::_thesis: A in MSFixPoints F
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in (MSFixPoints F) . i )
assume A3: i in I ; ::_thesis: A . i in (MSFixPoints F) . i
then reconsider f = F . i as Function of (M . i),(M . i) by PBOOLE:def_15;
 i in dom F by A3, PARTFUN1:def_2;
then A4: f . (A . i) = A . i by A2, PRALG_1:def_17;
 M = doms F by MSSUBFAM:17;
then  M . i = dom f by A3, MSSUBFAM:14;
then  A . i in dom f by A1, A3, PBOOLE:def_1;
hence  A . i in (MSFixPoints F) . i by A3, A4, Def12; ::_thesis: verum
end;
assume A5: A in MSFixPoints F ; ::_thesis: ( A in M & F .. A = A )
thus  A in M ::_thesis: F .. A = A
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in M . i )
A6: M = doms F by MSSUBFAM:17;
assume A7: i in I ; ::_thesis: A . i in M . i
then  A . i in (MSFixPoints F) . i by A5, PBOOLE:def_1;
then  ex f being Function st
( f = F . i & A . i in dom f & f . (A . i) = A . i ) by A7, Def12;
hence  A . i in M . i by A7, A6, MSSUBFAM:14; ::_thesis: verum
end;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(F_.._A)_._i_=_A_._i
let i be set ; ::_thesis: ( i in I implies (F .. A) . i = A . i )
assume A8: i in I ; ::_thesis: (F .. A) . i = A . i
then  A . i in (MSFixPoints F) . i by A5, PBOOLE:def_1;
then A9: ex f being Function st
( f = F . i & A . i in dom f & f . (A . i) = A . i ) by A8, Def12;
 i in dom F by A8, PARTFUN1:def_2;
hence  (F .. A) . i = A . i by A9, PRALG_1:def_17; ::_thesis: verum
end;
hence  F .. A = A by PBOOLE:3; ::_thesis: verum
end;

theorem :: CLOSURE1:29
for I being set
for A being ManySortedSet of I holds MSFixPoints (id A) = A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds MSFixPoints (id A) = A
let A be ManySortedSet of I; ::_thesis: MSFixPoints (id A) = A
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(MSFixPoints_(id_A))_._i_=_A_._i
let i be set ; ::_thesis: ( i in I implies (MSFixPoints (id A)) . i = A . i )
assume A1: i in I ; ::_thesis: (MSFixPoints (id A)) . i = A . i
thus  (MSFixPoints (id A)) . i = A . i ::_thesis: verum
proof
thus  (MSFixPoints (id A)) . i c= A . i :: according to XBOOLE_0:def_10 ::_thesis: A . i c= (MSFixPoints (id A)) . i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (MSFixPoints (id A)) . i or x in A . i )
assume  x in (MSFixPoints (id A)) . i ; ::_thesis: x in A . i
then consider f being Function such that
A2: f = (id A) . i and
A3: x in dom f and
 f . x = x by A1, Def12;
 f is Function of (A . i),(A . i) by A1, A2, PBOOLE:def_15;
hence  x in A . i by A3, FUNCT_2:52; ::_thesis: verum
end;
reconsider f = (id A) . i as Function of (A . i),(A . i) by A1, PBOOLE:def_15;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in (MSFixPoints (id A)) . i )
assume A4: x in A . i ; ::_thesis: x in (MSFixPoints (id A)) . i
A5: x in dom f by A4, FUNCT_2:52;
 f = id (A . i) by A1, MSUALG_3:def_1;
then  f . x = x by A4, FUNCT_1:18;
hence  x in (MSFixPoints (id A)) . i by A1, A5, Def12; ::_thesis: verum
end;
end;
hence  MSFixPoints (id A) = A by PBOOLE:3; ::_thesis: verum
end;

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
proof
let S be 1-sorted ; ::_thesis: 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
let A be ManySortedSet of the carrier of S; ::_thesis: 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
let J be reflexive monotonic MSSetOp of A; ::_thesis: for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S
let D be MSSubsetFamily of A; ::_thesis: ( D = MSFixPoints J implies MSClosureStr(# A,D #) is MSClosureSystem of S )
assume A1: D = MSFixPoints J ; ::_thesis: MSClosureStr(# A,D #) is MSClosureSystem of S
 D is absolutely-multiplicative
proof
let F be MSSubsetFamily of A; :: according to MSSUBFAM:def_5 ::_thesis: ( not F c= D or meet F in D )
assume A2: F c= D ; ::_thesis: meet F in D
A3: J .. (meet F) c= meet F
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or (J .. (meet F)) . i c= (meet F) . i )
assume A4: i in the carrier of S ; ::_thesis: (J .. (meet F)) . i c= (meet F) . i
then reconsider j = J . i as Function of ((bool A) . i),((bool A) . i) by PBOOLE:def_15;
A5: i in dom J by A4, PARTFUN1:def_2;
consider Q being Subset-Family of (A . i) such that
A6: Q = F . i and
A7: (meet F) . i = Intersect Q by A4, MSSUBFAM:def_1;
A8: now__::_thesis:_for_x_being_set_st_x_in_Q_holds_
j_._(Intersect_Q)_c=_x
let x be set ; ::_thesis: ( x in Q implies j . (Intersect Q) c= x )
assume A9: x in Q ; ::_thesis: j . (Intersect Q) c= x
 Q c= D . i by A2, A4, A6, PBOOLE:def_2;
then  ex jj being Function st
( jj = J . i & x in dom jj & jj . x = x ) by A1, A4, A9, Def12;
hence  j . (Intersect Q) c= x by A4, A9, Th25, MSSUBFAM:2; ::_thesis: verum
end;
 (bool A) . i = bool (A . i) by A4, MBOOLEAN:def_1;
then  j . (Intersect Q) in bool (A . i) by FUNCT_2:5;
then  j . (Intersect Q) c= Intersect Q by A8, MSSUBFAM:4;
hence  (J .. (meet F)) . i c= (meet F) . i by A7, A5, PRALG_1:def_17; ::_thesis: verum
end;
 meet F c= A by PBOOLE:def_18;
then A10: meet F in bool A by MBOOLEAN:18;
then  meet F is Element of bool A by MSSUBFAM:11;
then  meet F c= J .. (meet F) by Def1;
then  J .. (meet F) = meet F by A3, PBOOLE:146;
hence  meet F in D by A1, A10, Th28; ::_thesis: verum
end;
hence  MSClosureStr(# A,D #) is MSClosureSystem of S ; ::_thesis: verum
end;

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 & X c= Y ) )
proof
let I be set ; ::_thesis: 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 & X c= Y ) )
let M be ManySortedSet of I; ::_thesis: 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 & X c= Y ) )
let D be properly-upper-bound MSSubsetFamily of M; ::_thesis: 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 & X c= Y ) )
let X be Element of bool M; ::_thesis: ex SF being V8() MSSubsetFamily of M st
for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) )
defpred S1[ set , set ] means X . $1 c= $2;
consider SF being ManySortedSet of I such that
A1: for i being set st i in I holds
for e being set holds
( e in SF . i iff ( e in D . i & S1[i,e] ) ) from PBOOLE:sch_2();
A2: D c= bool M by PBOOLE:def_18;
 SF is ManySortedSubset of bool M
proof
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or SF . i c= (bool M) . i )
assume A3: i in I ; ::_thesis: SF . i c= (bool M) . i
then  D . i c= (bool M) . i by A2, PBOOLE:def_2;
then A4: D . i c= bool (M . i) by A3, MBOOLEAN:def_1;
 SF . i c= bool (M . i)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SF . i or x in bool (M . i) )
assume  x in SF . i ; ::_thesis: x in bool (M . i)
then  x in D . i by A1, A3;
hence  x in bool (M . i) by A4; ::_thesis: verum
end;
hence  SF . i c= (bool M) . i by A3, MBOOLEAN:def_1; ::_thesis: verum
end;
then reconsider SF = SF as ManySortedSubset of bool M ;
reconsider SF = SF as MSSubsetFamily of M ;
 SF is V8()
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not SF . i is empty )
assume A5: i in I ; ::_thesis: not SF . i is empty
 M in D by MSSUBFAM:def_6;
then A6: M . i in D . i by A5, PBOOLE:def_1;
 X in bool M by MSSUBFAM:12;
then  X c= M by MBOOLEAN:18;
then  X . i c= M . i by A5, PBOOLE:def_2;
hence  not SF . i is empty by A1, A5, A6; ::_thesis: verum
end;
then reconsider SF = SF as V8() MSSubsetFamily of M ;
take  SF ; ::_thesis: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) )
let Y be ManySortedSet of I; ::_thesis: ( Y in SF iff ( Y in D & X c= Y ) )
thus  ( Y in SF implies ( Y in D & X c= Y ) ) ::_thesis: ( Y in D & X c= Y implies Y in SF )
proof
assume A7: Y in SF ; ::_thesis: ( Y in D & X c= Y )
thus  Y in D ::_thesis: X c= Y
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or Y . i in D . i )
assume A8: i in I ; ::_thesis: Y . i in D . i
then  Y . i in SF . i by A7, PBOOLE:def_1;
hence  Y . i in D . i by A1, A8; ::_thesis: verum
end;
thus  X c= Y ::_thesis: verum
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= Y . i )
assume A9: i in I ; ::_thesis: X . i c= Y . i
then  Y . i in SF . i by A7, PBOOLE:def_1;
hence  X . i c= Y . i by A1, A9; ::_thesis: verum
end;
end;
assume A10: ( Y in D & X c= Y ) ; ::_thesis: Y in SF
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or Y . i in SF . i )
assume A11: i in I ; ::_thesis: Y . i in SF . i
then  ( Y . i in D . i & X . i c= Y . i ) by A10, PBOOLE:def_1, PBOOLE:def_2;
hence  Y . i in SF . i by A1, A11; ::_thesis: verum
end;

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 & X c= Y ) ) ) holds
for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }
proof
let I be set ; ::_thesis: 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 & X c= Y ) ) ) holds
for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }
let M be ManySortedSet of I; ::_thesis: 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 & X c= Y ) ) ) holds
for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }
let D be properly-upper-bound MSSubsetFamily of M; ::_thesis: 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 & X c= Y ) ) ) holds
for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }
let X be Element of bool M; ::_thesis: for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }
let SF be V8() MSSubsetFamily of M; ::_thesis: ( ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) implies for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }  )
assume A1: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ; ::_thesis: for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }
let i be set ; ::_thesis: for Di being non empty set st i in I & Di = D . i holds
SF . i =  {  z where z is Element of Di : X . i c= z  }
let Di be non empty set ; ::_thesis: ( i in I & Di = D . i implies SF . i =  {  z where z is Element of Di : X . i c= z  }  )
assume that
A2: i in I and
A3: Di = D . i ; ::_thesis: SF . i =  {  z where z is Element of Di : X . i c= z  }
thus  SF . i c=  {  z where z is Element of Di : X . i c= z  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  z where z is Element of Di : X . i c= z  }  c= SF . i
proof
consider K being ManySortedSet of I such that
A4: K in SF by PBOOLE:134;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SF . i or x in  {  z where z is Element of Di : X . i c= z  }  )
assume A5: x in SF . i ; ::_thesis: x in  {  z where z is Element of Di : X . i c= z  }
 dom (K +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider L = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A6: dom (i .--> x) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A7: L . i = (i .--> x) . i by A6, FUNCT_4:13
.= x by FUNCOP_1:72 ;
A8: L in SF
proof
let s be set ; :: according to PBOOLE:def_1 ::_thesis: ( not s in I or L . s in SF . s )
assume A9: s in I ; ::_thesis: L . s in SF . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: L . s in SF . s
hence  L . s in SF . s by A5, A7; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: L . s in SF . s
then  not s in dom (i .--> x) by A6, TARSKI:def_1;
then  L . s = K . s by FUNCT_4:11;
hence  L . s in SF . s by A4, A9, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
then  X c= L by A1;
then A10: X . i c= L . i by A2, PBOOLE:def_2;
 L in D by A1, A8;
then  L . i in D . i by A2, PBOOLE:def_1;
hence  x in  {  z where z is Element of Di : X . i c= z  }  by A3, A7, A10; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  z where z is Element of Di : X . i c= z  }  or x in SF . i )
assume  x in  {  z where z is Element of Di : X . i c= z  }  ; ::_thesis: x in SF . i
then consider g being Element of Di such that
A11: g = x and
A12: X . i c= g ;
 dom (M +* (i .--> g)) = I by A2, PZFMISC1:1;
then reconsider L1 = M +* (i .--> g) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A13: dom (i .--> g) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A14: L1 . i = (i .--> g) . i by A13, FUNCT_4:13
.= g by FUNCOP_1:72 ;
A15: X c= L1
proof
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in I or X . s c= L1 . s )
assume A16: s in I ; ::_thesis: X . s c= L1 . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X . s c= L1 . s
hence  X . s c= L1 . s by A12, A14; ::_thesis: verum
end;
supposeA17: s <> i ; ::_thesis: X . s c= L1 . s
 X in bool M by MSSUBFAM:12;
then A18: X c= M by MBOOLEAN:18;
 not s in dom (i .--> g) by A13, A17, TARSKI:def_1;
then  L1 . s = M . s by FUNCT_4:11;
hence  X . s c= L1 . s by A16, A18, PBOOLE:def_2; ::_thesis: verum
end;
end;
end;
A19: M in D by MSSUBFAM:def_6;
 L1 in D
proof
let s be set ; :: according to PBOOLE:def_1 ::_thesis: ( not s in I or L1 . s in D . s )
assume A20: s in I ; ::_thesis: L1 . s in D . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: L1 . s in D . s
hence  L1 . s in D . s by A3, A14; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: L1 . s in D . s
then  not s in dom (i .--> g) by A13, TARSKI:def_1;
then  L1 . s = M . s by FUNCT_4:11;
hence  L1 . s in D . s by A19, A20, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
then  L1 in SF by A1, A15;
hence  x in SF . i by A2, A11, A14, PBOOLE:def_1; ::_thesis: verum
end;

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 & X c= Y ) ) ) holds
J .. X = meet SF
proof
let I be set ; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF
let M be ManySortedSet of I; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF
let D be properly-upper-bound MSSubsetFamily of M; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF
set G = bool M;
defpred S1[ set , set , set ] means  for sf being Subset-Family of (M . $3)
for Fi being non empty set st Fi = D . $3 & sf =  {  z where z is Element of Fi : $2 c= z  }  holds
$1 = Intersect sf;
A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
for_x_being_set_st_x_in_(bool_M)_._i_holds_
ex_y_being_set_st_
(_y_in_(bool_M)_._i_&_S1[y,x,i]_)
consider K being ManySortedSet of I such that
A2: K in bool M by PBOOLE:134;
let i be set ; ::_thesis: ( i in I implies for x being set st x in (bool M) . i holds
ex y being set st
( y in (bool M) . i & S1[y,x,i] ) )
assume A3: i in I ; ::_thesis: for x being set st x in (bool M) . i holds
ex y being set st
( y in (bool M) . i & S1[y,x,i] )
reconsider b = (bool M) . i as non empty set by A3;
let x be set ; ::_thesis: ( x in (bool M) . i implies ex y being set st
( y in (bool M) . i & S1[y,x,i] ) )
assume A4: x in (bool M) . i ; ::_thesis: ex y being set st
( y in (bool M) . i & S1[y,x,i] )
 dom (K +* (i .--> x)) = I by A3, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> x) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A6: X . i = (i .--> x) . i by A5, FUNCT_4:13
.= x by FUNCOP_1:72 ;
A7: X is Element of bool M
proof
let s be set ; :: according to PBOOLE:def_14 ::_thesis: ( not s in I or X . s is Element of (bool M) . s )
assume A8: s in I ; ::_thesis: X . s is Element of (bool M) . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X . s is Element of (bool M) . s
hence  X . s is Element of (bool M) . s by A4, A6; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X . s is Element of (bool M) . s
then  not s in dom (i .--> x) by A5, TARSKI:def_1;
then  X . s = K . s by FUNCT_4:11;
hence  X . s is Element of (bool M) . s by A2, A8, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
then consider SF being V8() MSSubsetFamily of M such that
A9: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
reconsider sf = SF . i as Subset-Family of (M . i) by A3, MSSUBFAM:32;
reconsider q = Intersect sf as Element of b by A3, MBOOLEAN:def_1;
reconsider s = b --> q as Function of b,b ;
take y = s . x; ::_thesis: ( y in (bool M) . i & S1[y,x,i] )
 Intersect sf in bool (M . i) ;
then  Intersect sf in b by A3, MBOOLEAN:def_1;
hence  y in (bool M) . i by A4, FUNCOP_1:7; ::_thesis: S1[y,x,i]
thus  S1[y,x,i] ::_thesis: verum
proof
reconsider Di = D . i as non empty set by A3;
A10: SF . i =  {  z where z is Element of Di : X . i c= z  }  by A3, A7, A9, Th32;
let sf1 be Subset-Family of (M . i); ::_thesis: for Fi being non empty set st Fi = D . i & sf1 =  {  z where z is Element of Fi : x c= z  }  holds
y = Intersect sf1
let Fi be non empty set ; ::_thesis: ( Fi = D . i & sf1 =  {  z where z is Element of Fi : x c= z  }  implies y = Intersect sf1 )
assume  ( Fi = D . i & sf1 =  {  z where z is Element of Fi : x c= z  }  ) ; ::_thesis: y = Intersect sf1
hence  y = Intersect sf1 by A4, A6, A10, FUNCOP_1:7; ::_thesis: verum
end;
end;
consider J being ManySortedFunction of bool M, bool M such that
A11: for i being set st i in I holds
ex f being Function of ((bool M) . i),((bool M) . i) st
( f = J . i & ( for x being set st x in (bool M) . i holds
S1[f . x,x,i] ) ) from MSSUBFAM:sch_1(A1);
reconsider J = J as MSSetOp of M ;
take  J ; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF
let X be Element of bool M; ::_thesis: for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF
let SF be V8() MSSubsetFamily of M; ::_thesis: ( ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) implies J .. X = meet SF )
assume A12: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ; ::_thesis: J .. X = meet SF
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(J_.._X)_._i_=_(meet_SF)_._i
let i be set ; ::_thesis: ( i in I implies (J .. X) . i = (meet SF) . i )
assume A13: i in I ; ::_thesis: (J .. X) . i = (meet SF) . i
then consider Q being Subset-Family of (M . i) such that
A14: Q = SF . i and
A15: (meet SF) . i = Intersect Q by MSSUBFAM:def_1;
reconsider Fi = D . i as non empty set by A13;
A16: Q =  {  z where z is Element of Fi : X . i c= z  }  by A12, A13, A14, Th32;
 X in bool M by MSSUBFAM:12;
then A17: X . i in (bool M) . i by A13, PBOOLE:def_1;
consider f being Function of ((bool M) . i),((bool M) . i) such that
A18: f = J . i and
A19: for x being set st x in (bool M) . i holds
S1[f . x,x,i] by A11, A13;
 dom J = I by PARTFUN1:def_2;
hence (J .. X) . i = f . (X . i) by A13, A18, PRALG_1:def_17
.= (meet SF) . i by A19, A15, A16, A17 ;
::_thesis: verum
end;
hence  J .. X = meet SF by PBOOLE:3; ::_thesis: verum
end;

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 & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J .. A = A
proof
let I be set ; ::_thesis: 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 & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J .. A = A
let M be ManySortedSet of I; ::_thesis: 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 & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J .. A = A
let D be properly-upper-bound MSSubsetFamily of M; ::_thesis: for A being Element of bool M
for J being MSSetOp of M st A in D & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J .. A = A
let A be Element of bool M; ::_thesis: for J being MSSetOp of M st A in D & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J .. A = A
let J be MSSetOp of M; ::_thesis: ( A in D & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) implies J .. A = A )
assume that
A1: A in D and
A2: 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 & X c= Y ) ) ) holds
J .. X = meet SF ; ::_thesis: J .. A = A
consider SF being V8() MSSubsetFamily of M such that
A3: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & A c= Y ) ) by Th31;
 A in SF by A1, A3;
then  meet SF c= A by MSSUBFAM:43;
then A4: J .. A c= A by A2, A3;
A5: for Z1 being ManySortedSet of I st Z1 in SF holds
A c= Z1 by A3;
 J .. A = meet SF by A2, A3;
then  A c= J .. A by A5, MSSUBFAM:45;
hence  J .. A = A by A4, PBOOLE:146; ::_thesis: verum
end;

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 & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
A in D
proof
let I be set ; ::_thesis: 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 & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
A in D
let M be ManySortedSet of I; ::_thesis: 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 & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
A in D
let D be absolutely-multiplicative MSSubsetFamily of M; ::_thesis: for A being Element of bool M
for J being MSSetOp of M st J .. A = A & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
A in D
let A be Element of bool M; ::_thesis: for J being MSSetOp of M st J .. A = A & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
A in D
let J be MSSetOp of M; ::_thesis: ( J .. A = A & ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) implies A in D )
assume that
A1: J .. A = A and
A2: 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 & X c= Y ) ) ) holds
J .. X = meet SF ; ::_thesis: A in D
defpred S1[ ManySortedSet of I] means A c= $1;
consider SF being V8() MSSubsetFamily of M such that
A3: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & A c= Y ) ) by Th31;
A4: ( ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & S1[Y] ) ) ) implies SF c= D ) from CLOSURE1:sch_1();
 J .. A = meet SF by A2, A3;
hence  A in D by A1, A3, A4, MSSUBFAM:def_5; ::_thesis: verum
end;

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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
( J is reflexive & J is monotonic )
proof
let I be set ; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
( J is reflexive & J is monotonic )
let M be ManySortedSet of I; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
( J is reflexive & J is monotonic )
let D be properly-upper-bound MSSubsetFamily of M; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
( J is reflexive & J is monotonic )
let J be MSSetOp of M; ::_thesis: ( ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) implies ( J is reflexive & J is monotonic ) )
assume A1: 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 & X c= Y ) ) ) holds
J .. X = meet SF ; ::_thesis: ( J is reflexive & J is monotonic )
thus  J is reflexive ::_thesis: J is monotonic
proof
let X be Element of bool M; :: according to CLOSURE1:def_1 ::_thesis: X c= J .. X
consider SF being V8() MSSubsetFamily of M such that
A2: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
 ( J .. X = meet SF & ( for Z1 being ManySortedSet of I st Z1 in SF holds
X c= Z1 ) ) by A1, A2;
hence  X c= J .. X by MSSUBFAM:45; ::_thesis: verum
end;
thus  J is monotonic ::_thesis: verum
proof
let x, y be Element of bool M; :: according to CLOSURE1:def_2 ::_thesis: ( x c= y implies J .. x c= J .. y )
assume A3: x c= y ; ::_thesis: J .. x c= J .. y
consider SFx being V8() MSSubsetFamily of M such that
A4: for Y being ManySortedSet of I holds
( Y in SFx iff ( Y in D & x c= Y ) ) by Th31;
consider SFy being V8() MSSubsetFamily of M such that
A5: for Y being ManySortedSet of I holds
( Y in SFy iff ( Y in D & y c= Y ) ) by Th31;
 SFy c= SFx
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or SFy . i c= SFx . i )
assume A6: i in I ; ::_thesis: SFy . i c= SFx . i
then consider Fi being non empty set  such that
A7: Fi = D . i ;
A8: x . i c= y . i by A3, A6, PBOOLE:def_2;
 ( SFx . i =  {  t where t is Element of Fi : x . i c= t  }  & SFy . i =  {  z where z is Element of Fi : y . i c= z  }  ) by A4, A5, A6, A7, Th32;
hence  SFy . i c= SFx . i by A8, Th1; ::_thesis: verum
end;
then A9: meet SFx c= meet SFy by MSSUBFAM:46;
 J .. x = meet SFx by A1, A4;
hence  J .. x c= J .. y by A1, A5, A9; ::_thesis: verum
end;
end;

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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent
proof
let I be set ; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent
let M be ManySortedSet of I; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent
let D be absolutely-multiplicative MSSubsetFamily of M; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent
let J be MSSetOp of M; ::_thesis: ( ( 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 & X c= Y ) ) ) holds
J .. X = meet SF ) implies J is idempotent )
assume A1: 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 & X c= Y ) ) ) holds
J .. X = meet SF ; ::_thesis: J is idempotent
let X be Element of bool M; :: according to CLOSURE1:def_3 ::_thesis: J .. X = J .. (J .. X)
defpred S1[ ManySortedSet of I] means X c= $1;
consider SF being V8() MSSubsetFamily of M such that
A2: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
 ( ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & S1[Y] ) ) ) implies SF c= D ) from CLOSURE1:sch_1();
then A3: meet SF in D by A2, MSSUBFAM:def_5;
 D c= bool M by PBOOLE:def_18;
then A4: meet SF is Element of bool M by A3, MSSUBFAM:11, PBOOLE:9;
thus J .. X = meet SF by A1, A2
.= J .. (meet SF) by A1, A3, A4, Th34
.= J .. (J .. X) by A1, A2 ; ::_thesis: verum
end;

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 & 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 & it = MSClosureStr(# A,D #) );
existence
 ex b1 being MSClosureSystem of S ex D being MSSubsetFamily of A st
( D = MSFixPoints C & b1 = MSClosureStr(# A,D #) )
proof
reconsider D = MSFixPoints C as MSSubsetFamily of A ;
reconsider a = MSClosureStr(# A,D #) as MSClosureSystem of S by Th30;
take  a ; ::_thesis: ex D being MSSubsetFamily of A st
( D = MSFixPoints C & a = MSClosureStr(# A,D #) )
thus  ex D being MSSubsetFamily of A st
( D = MSFixPoints C & a = MSClosureStr(# A,D #) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being MSClosureSystem of S st ex D being MSSubsetFamily of A st
( D = MSFixPoints C & b1 = MSClosureStr(# A,D #) ) & ex D being MSSubsetFamily of A st
( D = MSFixPoints C & 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 & 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
proof
 ex D being MSSubsetFamily of A st
( D = MSFixPoints C & ClOp->ClSys C = MSClosureStr(# A,D #) ) by Def13;
hence  ClOp->ClSys C is strict ; ::_thesis: verum
end;
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
proof
 ex D being MSSubsetFamily of A st
( D = MSFixPoints C & ClOp->ClSys C = MSClosureStr(# A,D #) ) by Def13;
hence  ClOp->ClSys C is non-empty ; ::_thesis: verum
end;
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 & 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 & X c= Y ) ) ) holds
b1 .. X = meet SF
proof
consider J being MSSetOp of the Sorts of D such that
A1: 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 & X c= Y ) ) ) holds
J .. X = meet SF by Th33;
reconsider J = J as MSClosureOperator of the Sorts of D by A1, Th36, Th37;
take  J ; ::_thesis: 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 & X c= Y ) ) ) holds
J .. X = meet SF
thus  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 & X c= Y ) ) ) holds
J .. X = meet SF by A1; ::_thesis: verum
end;
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 & X c= Y ) ) ) holds
b1 .. X = meet SF ) & ( 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 & X c= Y ) ) ) holds
b2 .. X = meet SF ) holds
b1 = b2
proof
set M = the Sorts of D;
let Q1, Q2 be MSClosureOperator of the Sorts of D; ::_thesis: ( ( 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 & X c= Y ) ) ) holds
Q1 .. X = meet SF ) & ( 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 & X c= Y ) ) ) holds
Q2 .. X = meet SF ) implies Q1 = Q2 )
assume that
A2: 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 & X c= Y ) ) ) holds
Q1 .. X = meet SF and
A3: 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 & X c= Y ) ) ) holds
Q2 .. X = meet SF ; ::_thesis: Q1 = Q2
now__::_thesis:_for_x_being_ManySortedSet_of_the_carrier_of_S_st_x_in_bool_the_Sorts_of_D_holds_
Q1_.._x_=_Q2_.._x
let x be ManySortedSet of the carrier of S; ::_thesis: ( x in bool the Sorts of D implies Q1 .. x = Q2 .. x )
assume  x in bool the Sorts of D ; ::_thesis: Q1 .. x = Q2 .. x
then A4: x is Element of bool the Sorts of D by MSSUBFAM:11;
then consider SF being V8() MSSubsetFamily of the Sorts of D such that
A5: for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & x c= Y ) ) by Th31;
thus Q1 .. x = meet SF by A2, A4, A5
.= Q2 .. x by A3, A4, A5 ; ::_thesis: verum
end;
hence  Q1 = Q2 by Th7; ::_thesis: verum
end;
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 & 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
proof
let S be 1-sorted ; ::_thesis: for A being ManySortedSet of the carrier of S
for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J
let A be ManySortedSet of the carrier of S; ::_thesis: for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J
let J be MSClosureOperator of A; ::_thesis: ClSys->ClOp (ClOp->ClSys J) = J
set I = the carrier of S;
set M = the Sorts of (ClOp->ClSys J);
set j = ClSys->ClOp (ClOp->ClSys J);
A1: ex D being MSSubsetFamily of A st
( D = MSFixPoints J & ClOp->ClSys J = MSClosureStr(# A,D #) ) by Def13;
 for X being ManySortedSet of the carrier of S st X in bool A holds
(ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X
proof
let X be ManySortedSet of the carrier of S; ::_thesis: ( X in bool A implies (ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X )
assume  X in bool A ; ::_thesis: (ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X
then A2: X is Element of bool the Sorts of (ClOp->ClSys J) by A1, MSSUBFAM:11;
then consider SF being V8() MSSubsetFamily of the Sorts of (ClOp->ClSys J) such that
A3: for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in MSFixPoints J & X c= Y ) ) by A1, Th31;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
((ClSys->ClOp_(ClOp->ClSys_J))_.._X)_._i_=_(J_.._X)_._i
A4: dom J = the carrier of S by PARTFUN1:def_2;
let i be set ; ::_thesis: ( i in the carrier of S implies ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i )
assume A5: i in the carrier of S ; ::_thesis: ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = (J .. X) . i
reconsider f = J . i as Function of ((bool A) . i),((bool A) . i) by A5, PBOOLE:def_15;
 (bool A) . i = bool (A . i) by A5, MBOOLEAN:def_1;
then reconsider f = f as Function of (bool (A . i)),(bool (A . i)) ;
 X . i is Element of (bool A) . i by A1, A2, A5, PBOOLE:def_14;
then A6: X . i is Element of bool (A . i) by A5, MBOOLEAN:def_1;
then A7: X . i c= f . (X . i) by A5, Th24;
reconsider Di = (MSFixPoints J) . i as non empty set by A1, A5;
consider Q being Subset-Family of ( the Sorts of (ClOp->ClSys J) . i) such that
A8: Q = SF . i and
A9: (meet SF) . i = Intersect Q by A5, MSSUBFAM:def_1;
A10: SF . i =  {  z where z is Element of Di : X . i c= z  }  by A1, A2, A3, A5, Th32;
now__::_thesis:_for_x_being_set_st_x_in_Q_holds_
f_._(X_._i)_c=_x
let x be set ; ::_thesis: ( x in Q implies f . (X . i) c= x )
assume  x in Q ; ::_thesis: f . (X . i) c= x
then consider x1 being Element of Di such that
A11: ( x1 = x & X . i c= x1 ) by A8, A10;
 MSFixPoints J c= bool A by PBOOLE:def_18;
then  Di c= (bool A) . i by A5, PBOOLE:def_2;
then  Di c= bool (A . i) by A5, MBOOLEAN:def_1;
then A12: x1 is Element of bool (A . i) by TARSKI:def_3;
 ex g being Function st
( g = J . i & x1 in dom g & g . x1 = x1 ) by A5, Def12;
hence  f . (X . i) c= x by A5, A6, A11, A12, Th25; ::_thesis: verum
end;
then A13: f . (X . i) c= Intersect Q by A5, A8, MSSUBFAM:5;
A14: ( dom f = bool (A . i) & f . (X . i) in bool (A . i) ) by A6, FUNCT_2:5, FUNCT_2:def_1;
 f . (f . (X . i)) = f . (X . i) by A5, A6, Th26;
then  f . (X . i) is Element of Di by A5, A14, Def12;
then  f . (X . i) in  {  z where z is Element of Di : X . i c= z  }  by A7;
then  Intersect Q c= f . (X . i) by A8, A10, MSSUBFAM:2;
then  Intersect Q = f . (X . i) by A13, XBOOLE_0:def_10;
hence ((ClSys->ClOp (ClOp->ClSys J)) .. X) . i = f . (X . i) by A1, A2, A3, A9, Def14
.= (J .. X) . i by A5, A4, PRALG_1:def_17 ;
::_thesis: verum
end;
hence  (ClSys->ClOp (ClOp->ClSys J)) .. X = J .. X by PBOOLE:3; ::_thesis: verum
end;
hence  ClSys->ClOp (ClOp->ClSys J) = J by A1, Th7; ::_thesis: verum
end;

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 #)
proof
let S be 1-sorted ; ::_thesis: for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)
let D be MSClosureSystem of S; ::_thesis: ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)
set M = the Sorts of D;
set F = the Family of D;
set I = the carrier of S;
consider X1 being ManySortedSet of the carrier of S such that
A1: X1 in bool the Sorts of D by PBOOLE:134;
 the Family of D = MSFixPoints (ClSys->ClOp D)
proof
A2: dom (ClSys->ClOp D) = the carrier of S by PARTFUN1:def_2;
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( not i in the carrier of S or the Family of D . i = (MSFixPoints (ClSys->ClOp D)) . i )
assume A3: i in the carrier of S ; ::_thesis: the Family of D . i = (MSFixPoints (ClSys->ClOp D)) . i
reconsider f = (ClSys->ClOp D) . i as Function of ((bool the Sorts of D) . i),((bool the Sorts of D) . i) by A3, PBOOLE:def_15;
reconsider Fi = the Family of D . i as non empty set by A3;
thus  the Family of D . i c= (MSFixPoints (ClSys->ClOp D)) . i :: according to XBOOLE_0:def_10 ::_thesis: (MSFixPoints (ClSys->ClOp D)) . i c= the Family of D . i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Family of D . i or x in (MSFixPoints (ClSys->ClOp D)) . i )
assume A4: x in the Family of D . i ; ::_thesis: x in (MSFixPoints (ClSys->ClOp D)) . i
 dom (X1 +* (i .--> x)) = the carrier of S by A3, PZFMISC1:1;
then reconsider X = X1 +* (i .--> x) as ManySortedSet of the carrier of S by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> x) = {i} by FUNCOP_1:13;
 the Family of D c= bool the Sorts of D by PBOOLE:def_18;
then A6: the Family of D . i c= (bool the Sorts of D) . i by A3, PBOOLE:def_2;
then  x in (bool the Sorts of D) . i by A4;
then A7: x in dom f by FUNCT_2:def_1;
 i in {i} by TARSKI:def_1;
then A8: X . i = (i .--> x) . i by A5, FUNCT_4:13
.= x by FUNCOP_1:72 ;
 X is Element of bool the Sorts of D
proof
let s be set ; :: according to PBOOLE:def_14 ::_thesis: ( not s in the carrier of S or X . s is Element of (bool the Sorts of D) . s )
assume A9: s in the carrier of S ; ::_thesis: X . s is Element of (bool the Sorts of D) . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X . s is Element of (bool the Sorts of D) . s
hence  X . s is Element of (bool the Sorts of D) . s by A4, A8, A6; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X . s is Element of (bool the Sorts of D) . s
then  not s in dom (i .--> x) by A5, TARSKI:def_1;
then  X . s = X1 . s by FUNCT_4:11;
hence  X . s is Element of (bool the Sorts of D) . s by A1, A9, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
then reconsider X = X as Element of bool the Sorts of D ;
consider SF being V8() MSSubsetFamily of the Sorts of D such that
A10: for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) by Th31;
consider Q being Subset-Family of ( the Sorts of D . i) such that
A11: Q = SF . i and
A12: (meet SF) . i = Intersect Q by A3, MSSUBFAM:def_1;
A13: SF . i =  {  z where z is Element of Fi : X . i c= z  }  by A3, A10, Th32;
now__::_thesis:_for_Z1_being_set_st_Z1_in_Q_holds_
x_c=_Z1
let Z1 be set ; ::_thesis: ( Z1 in Q implies x c= Z1 )
assume  Z1 in Q ; ::_thesis: x c= Z1
then  ex q being Element of Fi st
( q = Z1 & X . i c= q ) by A11, A13;
hence  x c= Z1 by A8; ::_thesis: verum
end;
then A14: x c= Intersect Q by A3, A11, MSSUBFAM:5;
 x in  {  B where B is Element of Fi : x c= B  }  by A4;
then  Intersect Q c= x by A8, A11, A13, MSSUBFAM:2;
then A15: Intersect Q = x by A14, XBOOLE_0:def_10;
 (ClSys->ClOp D) .. X = meet SF by A10, Def14;
then  f . x = x by A3, A8, A12, A15, A2, PRALG_1:def_17;
hence  x in (MSFixPoints (ClSys->ClOp D)) . i by A3, A7, Def12; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (MSFixPoints (ClSys->ClOp D)) . i or x in the Family of D . i )
assume A16: x in (MSFixPoints (ClSys->ClOp D)) . i ; ::_thesis: x in the Family of D . i
then A17: ex f being Function st
( f = (ClSys->ClOp D) . i & x in dom f & f . x = x ) by A3, Def12;
 dom (X1 +* (i .--> x)) = the carrier of S by A3, PZFMISC1:1;
then reconsider X = X1 +* (i .--> x) as ManySortedSet of the carrier of S by PARTFUN1:def_2, RELAT_1:def_18;
A18: dom (i .--> x) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A19: X . i = (i .--> x) . i by A18, FUNCT_4:13
.= x by FUNCOP_1:72 ;
 MSFixPoints (ClSys->ClOp D) c= bool the Sorts of D by PBOOLE:def_18;
then A20: (MSFixPoints (ClSys->ClOp D)) . i c= (bool the Sorts of D) . i by A3, PBOOLE:def_2;
 X is Element of bool the Sorts of D
proof
let s be set ; :: according to PBOOLE:def_14 ::_thesis: ( not s in the carrier of S or X . s is Element of (bool the Sorts of D) . s )
assume A21: s in the carrier of S ; ::_thesis: X . s is Element of (bool the Sorts of D) . s
percases ( s = i or s <> i ) ;
suppose s = i ; ::_thesis: X . s is Element of (bool the Sorts of D) . s
hence  X . s is Element of (bool the Sorts of D) . s by A16, A19, A20; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X . s is Element of (bool the Sorts of D) . s
then  not s in dom (i .--> x) by A18, TARSKI:def_1;
then  X . s = X1 . s by FUNCT_4:11;
hence  X . s is Element of (bool the Sorts of D) . s by A1, A21, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
then reconsider X = X as Element of bool the Sorts of D ;
defpred S1[ ManySortedSet of the carrier of S] means X c= $1;
consider SF being V8() MSSubsetFamily of the Sorts of D such that
A22: for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) by Th31;
A23: dom (ClSys->ClOp D) = the carrier of S by PARTFUN1:def_2;
 ( ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & S1[Y] ) ) ) implies SF c= the Family of D ) from CLOSURE1:sch_1();
then A24: meet SF in the Family of D by A22, MSSUBFAM:def_5;
(meet SF) . i = ((ClSys->ClOp D) .. X) . i by A22, Def14
.= x by A3, A17, A19, A23, PRALG_1:def_17 ;
hence  x in the Family of D . i by A3, A24, PBOOLE:def_1; ::_thesis: verum
end;
hence  ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #) by Def13; ::_thesis: verum
end;