:: CLOSURE2 semantic presentation

begin


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

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

theorem :: CLOSURE2:1
for M being non empty set
for X, Y being Element of M st X c= Y holds
(id M) . X c= (id M) . Y
proof
let M be non empty set ; ::_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 FUNCT_1:18;
hence  (id M) . X c= (id M) . Y by A1, FUNCT_1:18; ::_thesis: verum
end;

theorem Th2: :: CLOSURE2:2
for I being non empty set
for A being ManySortedSet of I
for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
proof
let I be non empty set ; ::_thesis: for A being ManySortedSet of I
for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
let A be ManySortedSet of I; ::_thesis: for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
let B be ManySortedSubset of A; ::_thesis: rng B c= union (rng (bool A))
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng B or a in union (rng (bool A)) )
assume  a in rng B ; ::_thesis: a in union (rng (bool A))
then consider i being set  such that
A1: i in I and
A2: a = B . i by PBOOLE:138;
 ( i in dom (bool A) & bool (A . i) = (bool A) . i ) by A1, MBOOLEAN:def_1, PARTFUN1:def_2;
then A3: bool (A . i) in rng (bool A) by FUNCT_1:def_3;
 B c= A by PBOOLE:def_18;
then  B in bool A by MBOOLEAN:18;
then  B . i in (bool A) . i by A1, PBOOLE:def_1;
then  a in bool (A . i) by A1, A2, MBOOLEAN:def_1;
hence  a in union (rng (bool A)) by A3, TARSKI:def_4; ::_thesis: verum
end;

begin

definition
let I be set ;
let M be ManySortedSet of I;
defpred S1[ set ] means $1 is ManySortedSubset of M;
func Bool M ->  set  means :Def1: :: CLOSURE2:def 1
 for x being set holds
( x in it iff x is ManySortedSubset of M );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedSubset of M )
proof
percases ( not I is empty or I is empty ) ;
supposeA1: not I is empty ; ::_thesis: ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedSubset of M )
consider X being set  such that
A2: for e being set holds
( e in X iff ( e in Funcs (I,(union (rng (bool M)))) & S1[e] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff x is ManySortedSubset of M )
thus  for x being set holds
( x in X iff x is ManySortedSubset of M ) ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in X iff x is ManySortedSubset of M )
thus  ( x in X implies x is ManySortedSubset of M ) by A2; ::_thesis: ( x is ManySortedSubset of M implies x in X )
assume A3: x is ManySortedSubset of M ; ::_thesis: x in X
now__::_thesis:_(_x_in_Funcs_(I,(union_(rng_(bool_M))))_&_S1[x]_)
reconsider xx = x as ManySortedSubset of M by A3;
 ( dom xx = I & rng xx c= union (rng (bool M)) ) by A1, Th2, PARTFUN1:def_2;
hence  x in Funcs (I,(union (rng (bool M)))) by FUNCT_2:def_2; ::_thesis: S1[x]
thus  S1[x] by A3; ::_thesis: verum
end;
hence  x in X by A2; ::_thesis: verum
end;
end;
supposeA4: I is empty ; ::_thesis: ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedSubset of M )
take  {([[0]] {})} ; ::_thesis: for x being set holds
( x in {([[0]] {})} iff x is ManySortedSubset of M )
thus  for x being set holds
( x in {([[0]] {})} iff x is ManySortedSubset of M ) ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in {([[0]] {})} iff x is ManySortedSubset of M )
thus  ( x in {([[0]] {})} implies x is ManySortedSubset of M ) ::_thesis: ( x is ManySortedSubset of M implies x in {([[0]] {})} )
proof
reconsider M9 = M as ManySortedSet of {} by A4;
assume A6: x in {([[0]] {})} ; ::_thesis: x is ManySortedSubset of M
reconsider y = [[0]] {} as ManySortedSubset of M9 by PBOOLE:def_18;
 y is ManySortedSubset of M by A4;
hence  x is ManySortedSubset of M by A6, TARSKI:def_1; ::_thesis: verum
end;
assume  x is ManySortedSubset of M ; ::_thesis: x in {([[0]] {})}
then consider y being ManySortedSubset of M such that
A7: y = x ;
 y = [[0]] {} by A4;
hence  x in {([[0]] {})} by A7, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is ManySortedSubset of M ) ) & ( for x being set holds
( x in b2 iff x is ManySortedSubset of M ) ) holds
b1 = b2
proof
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

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

registration
let I be set ;
let M be ManySortedSet of I;
cluster Bool M ->  non empty functional with_common_domain ;
coherence
 ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain )
proof
 M is ManySortedSubset of M by PBOOLE:def_18;
hence  not Bool M is empty by Def1; ::_thesis: ( Bool M is functional & Bool M is with_common_domain )
thus  Bool M is functional ::_thesis: Bool M is with_common_domain
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in Bool M or x is set )
assume  x in Bool M ; ::_thesis: x is set
hence  x is set by Def1; ::_thesis: verum
end;
let f, g be Function; :: according to CARD_3:def_10 ::_thesis: ( not f in Bool M or not g in Bool M or dom f = dom g )
assume that
A1: f in Bool M and
A2: g in Bool M ; ::_thesis: dom f = dom g
A3: g is ManySortedSubset of M by A2, Def1;
 f is ManySortedSubset of M by A1, Def1;
hence  dom f = I by PARTFUN1:def_2
.= dom g by A3, PARTFUN1:def_2 ;
::_thesis: verum
end;
end;

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

definition
let I be set ;
let M be ManySortedSet of I;
:: original: Bool
redefine func Bool M ->  SubsetFamily of M;
coherence
 Bool M is SubsetFamily of M
proof
 Bool M c= Bool M ;
hence  Bool M is SubsetFamily of M ; ::_thesis: verum
end;
end;

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

registration
let I be set ;
let M be ManySortedSet of I;
cluster empty functional finite for Element of bool (Bool M);
existence
 ex b1 being SubsetFamily of M st
( b1 is empty & b1 is finite )
proof
reconsider x = {} as SubsetFamily of M by XBOOLE_1:2;
take  x ; ::_thesis: ( x is empty & x is finite )
thus  ( x is empty & x is finite ) ; ::_thesis: verum
end;
end;


definition
let I be set ;
let M be ManySortedSet of I;
let S be non empty SubsetFamily of M;
:: original: Element
redefine mode Element of S ->  ManySortedSubset of M;
coherence
 for b1 being Element of S holds b1 is ManySortedSubset of M
proof
let e be Element of S; ::_thesis: e is ManySortedSubset of M
thus  e is ManySortedSubset of M by Def1; ::_thesis: verum
end;
end;

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

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

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

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

theorem Th7: :: CLOSURE2:7
for I being set
for A, M being ManySortedSet of I st A c= M holds
{A} is SubsetFamily of M
proof
let I be set ; ::_thesis: for A, M being ManySortedSet of I st A c= M holds
{A} is SubsetFamily of M
let A, M be ManySortedSet of I; ::_thesis: ( A c= M implies {A} is SubsetFamily of M )
assume  A c= M ; ::_thesis: {A} is SubsetFamily of M
then  A is ManySortedSubset of M by PBOOLE:def_18;
then  A in Bool M by Def1;
hence  {A} is SubsetFamily of M by ZFMISC_1:31; ::_thesis: verum
end;

theorem Th8: :: CLOSURE2:8
for I being set
for A, M, B being ManySortedSet of I st A c= M & B c= M holds
{A,B} is SubsetFamily of M
proof
let I be set ; ::_thesis: for A, M, B being ManySortedSet of I st A c= M & B c= M holds
{A,B} is SubsetFamily of M
let A, M, B be ManySortedSet of I; ::_thesis: ( A c= M & B c= M implies {A,B} is SubsetFamily of M )
assume  ( A c= M & B c= M ) ; ::_thesis: {A,B} is SubsetFamily of M
then  ( {A} is SubsetFamily of M & {B} is SubsetFamily of M ) by Th7;
then  {A} \/ {B} is SubsetFamily of M by Th3;
hence  {A,B} is SubsetFamily of M by ENUMSET1:1; ::_thesis: verum
end;


theorem Th9: :: CLOSURE2:9
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E /\ T in Bool M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M holds E /\ T in Bool M
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M holds E /\ T in Bool M
let E, T be Element of Bool M; ::_thesis: E /\ T in Bool M
 ( E c= M & T c= M ) by PBOOLE:def_18;
then  E /\ T c= M /\ M by PBOOLE:21;
then  E /\ T is ManySortedSubset of M by PBOOLE:def_18;
hence  E /\ T in Bool M by Def1; ::_thesis: verum
end;

theorem Th10: :: CLOSURE2:10
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E \/ T in Bool M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M holds E \/ T in Bool M
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M holds E \/ T in Bool M
let E, T be Element of Bool M; ::_thesis: E \/ T in Bool M
 ( E c= M & T c= M ) by PBOOLE:def_18;
then  E \/ T c= M \/ M by PBOOLE:20;
then  E \/ T is ManySortedSubset of M by PBOOLE:def_18;
hence  E \/ T in Bool M by Def1; ::_thesis: verum
end;

theorem :: CLOSURE2:11
for I being set
for A, M being ManySortedSet of I
for E being Element of Bool M holds E \ A in Bool M
proof
let I be set ; ::_thesis: for A, M being ManySortedSet of I
for E being Element of Bool M holds E \ A in Bool M
let A, M be ManySortedSet of I; ::_thesis: for E being Element of Bool M holds E \ A in Bool M
let E be Element of Bool M; ::_thesis: E \ A in Bool M
 E c= M by PBOOLE:def_18;
then  E \ A c= M by MBOOLEAN:15;
then  E \ A is ManySortedSubset of M by PBOOLE:def_18;
hence  E \ A in Bool M by Def1; ::_thesis: verum
end;

theorem :: CLOSURE2:12
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E \+\ T in Bool M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M holds E \+\ T in Bool M
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M holds E \+\ T in Bool M
let E, T be Element of Bool M; ::_thesis: E \+\ T in Bool M
 T c= M by PBOOLE:def_18;
then A1: T \ E c= M by MBOOLEAN:15;
 E c= M by PBOOLE:def_18;
then  E \ T c= M by MBOOLEAN:15;
then  E \+\ T c= M by A1, PBOOLE:91;
then  E \+\ T is ManySortedSubset of M by PBOOLE:def_18;
hence  E \+\ T in Bool M by Def1; ::_thesis: verum
end;

begin

definition
let S be functional set ;
func|.S.| ->  Function means :Def2: :: CLOSURE2:def 2
 ex A being non empty functional set st
( A = S & dom it = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom it holds
it . i =  {  (x . i) where x is Element of A : verum  }  ) ) if S <> {}
otherwise it = {} ;
existence
 ( ( S <> {} implies ex b1 being Function ex A being non empty functional set st
( A = S & dom b1 = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom b1 holds
b1 . i =  {  (x . i) where x is Element of A : verum  }  ) ) ) & ( not S <> {} implies ex b1 being Function st b1 = {} ) )
proof
thus  ( S <> {} implies ex f being Function ex A being non empty functional set st
( A = S & dom f = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom f holds
f . i =  {  (x . i) where x is Element of A : verum  }  ) ) ) ::_thesis: ( not S <> {} implies ex b1 being Function st b1 = {} )
proof
assume  S <> {} ; ::_thesis: ex f being Function ex A being non empty functional set st
( A = S & dom f = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom f holds
f . i =  {  (x . i) where x is Element of A : verum  }  ) )
then consider A being non empty functional set  such that
A1: A = S ;
deffunc H1( set ) ->  set =  {  (x . $1) where x is Element of A : verum  }  ;
consider f being Function such that
A2: ( dom f = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in meet  {  (dom x) where x is Element of A : verum  }  holds
f . i = H1(i) ) ) from FUNCT_1:sch_3();
take  f ; ::_thesis: ex A being non empty functional set st
( A = S & dom f = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom f holds
f . i =  {  (x . i) where x is Element of A : verum  }  ) )
take  A ; ::_thesis: ( A = S & dom f = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom f holds
f . i =  {  (x . i) where x is Element of A : verum  }  ) )
thus  ( A = S & dom f = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom f holds
f . i =  {  (x . i) where x is Element of A : verum  }  ) ) by A1, A2; ::_thesis: verum
end;
thus  ( not S <> {} implies ex b1 being Function st b1 = {} ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function holds
( ( S <> {} & ex A being non empty functional set st
( A = S & dom b1 = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom b1 holds
b1 . i =  {  (x . i) where x is Element of A : verum  }  ) ) & ex A being non empty functional set st
( A = S & dom b2 = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom b2 holds
b2 . i =  {  (x . i) where x is Element of A : verum  }  ) ) implies b1 = b2 ) & ( not S <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let f, g be Function; ::_thesis: ( ( S <> {} & ex A being non empty functional set st
( A = S & dom f = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom f holds
f . i =  {  (x . i) where x is Element of A : verum  }  ) ) & ex A being non empty functional set st
( A = S & dom g = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom g holds
g . i =  {  (x . i) where x is Element of A : verum  }  ) ) implies f = g ) & ( not S <> {} & f = {} & g = {} implies f = g ) )
defpred S1[ Function] means  ex A being non empty functional set st
( A = S & dom $1 = meet  {  (dom x) where x is Element of A : verum  }  & ( for i being set st i in dom $1 holds
$1 . i =  {  (x . i) where x is Element of A : verum  }  ) );
thus  ( S <> {} & S1[f] & S1[g] implies f = g ) ::_thesis: ( not S <> {} & f = {} & g = {} implies f = g )
proof
assume that
 S <> {} and
A3: S1[f] and
A4: S1[g] ; ::_thesis: f = g
consider A being non empty functional set  such that
A5: A = S and
A6: dom f = meet  {  (dom x) where x is Element of A : verum  }  and
A7: for i being set st i in dom f holds
f . i =  {  (x . i) where x is Element of A : verum  }  by A3;
now__::_thesis:_for_a_being_set_st_a_in_meet__{__(dom_x)_where_x_is_Element_of_A_:_verum__}__holds_
f_._a_=_g_._a
let a be set ; ::_thesis: ( a in meet  {  (dom x) where x is Element of A : verum  }  implies f . a = g . a )
assume A8: a in meet  {  (dom x) where x is Element of A : verum  }  ; ::_thesis: f . a = g . a
hence f . a =  {  (x . a) where x is Element of A : verum  }  by A6, A7
.= g . a by A4, A5, A8 ;
::_thesis: verum
end;
hence  f = g by A4, A5, A6, FUNCT_1:2; ::_thesis: verum
end;
thus  ( not S <> {} & f = {} & g = {} implies f = g ) ; ::_thesis: verum
end;
consistency
 for b1 being Function holds verum ;
end;

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

theorem Th13: :: CLOSURE2:13
for I being set
for M being ManySortedSet of I
for SF being non empty SubsetFamily of M holds dom |.SF.| = I
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for SF being non empty SubsetFamily of M holds dom |.SF.| = I
let M be ManySortedSet of I; ::_thesis: for SF being non empty SubsetFamily of M holds dom |.SF.| = I
let SF be non empty SubsetFamily of M; ::_thesis: dom |.SF.| = I
consider A being non empty functional set  such that
A1: A = SF and
A2: dom |.SF.| = meet  {  (dom x) where x is Element of A : verum  }  and
 for i being set st i in dom |.SF.| holds
|.SF.| . i =  {  (x . i) where x is Element of A : verum  }  by Def2;
  {  (dom x) where x is Element of A : verum  }  = {I}
proof
thus   {  (dom x) where x is Element of A : verum  }  c= {I} :: according to XBOOLE_0:def_10 ::_thesis: {I} c=  {  (dom x) where x is Element of A : verum  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (dom x) where x is Element of A : verum  }  or a in {I} )
assume  a in  {  (dom x) where x is Element of A : verum  }  ; ::_thesis: a in {I}
then consider x being Element of A such that
A3: a = dom x ;
 x is Element of SF by A1;
then  a = I by A3, PARTFUN1:def_2;
hence  a in {I} by TARSKI:def_1; ::_thesis: verum
end;
set x = the Element of A;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {I} or a in  {  (dom x) where x is Element of A : verum  }  )
assume  a in {I} ; ::_thesis: a in  {  (dom x) where x is Element of A : verum  }
then A4: a = I by TARSKI:def_1;
 the Element of A is Element of SF by A1;
then  dom the Element of A = I by PARTFUN1:def_2;
hence  a in  {  (dom x) where x is Element of A : verum  }  by A4; ::_thesis: verum
end;
hence  dom |.SF.| = I by A2, SETFAM_1:10; ::_thesis: verum
end;

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

definition
let I be set ;
let M be ManySortedSet of I;
let S be SubsetFamily of M;
func|:S:| ->  ManySortedSet of I equals :Def3: :: CLOSURE2:def 3
|.S.| if S <> {}
otherwise  [[0]] I;
coherence
 ( ( S <> {} implies |.S.| is ManySortedSet of I ) & ( not S <> {} implies [[0]] I is ManySortedSet of I ) )
proof
thus  ( S <> {} implies |.S.| is ManySortedSet of I ) ::_thesis: ( not S <> {} implies [[0]] I is ManySortedSet of I )
proof
assume  S <> {} ; ::_thesis: |.S.| is ManySortedSet of I
then  dom |.S.| = I by Th13;
hence  |.S.| is ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; ::_thesis: verum
end;
thus  ( not S <> {} implies [[0]] I is ManySortedSet of I ) ; ::_thesis: verum
end;
consistency
 for b1 being ManySortedSet of I holds verum ;
end;

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

registration
let I be set ;
let M be ManySortedSet of I;
let S be empty SubsetFamily of M;
cluster|:S:| -> V9() ;
coherence
 |:S:| is empty-yielding
proof
 |:S:| = [[0]] I by Def3;
hence  |:S:| is empty-yielding ; ::_thesis: verum
end;
end;

theorem Th14: :: CLOSURE2:14
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }
let M be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }
let SF be SubsetFamily of M; ::_thesis: ( not SF is empty implies for i being set st i in I holds
|:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }  )
A1: dom |:SF:| = I by PARTFUN1:def_2;
assume A2: not SF is empty ; ::_thesis: for i being set st i in I holds
|:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }
then consider A being non empty functional set  such that
A3: A = SF and
 dom |.SF.| = meet  {  (dom x) where x is Element of A : verum  }  and
A4: for i being set st i in dom |.SF.| holds
|.SF.| . i =  {  (x . i) where x is Element of A : verum  }  by Def2;
let i be set ; ::_thesis: ( i in I implies |:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }  )
assume A5: i in I ; ::_thesis: |:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }
set K =  {  (x . i) where x is Element of Bool M : x in SF  }  ;
set N =  {  (x . i) where x is Element of A : verum  }  ;
A6:  {  (x . i) where x is Element of Bool M : x in SF  }  =  {  (x . i) where x is Element of A : verum  }
proof
thus   {  (x . i) where x is Element of Bool M : x in SF  }  c=  {  (x . i) where x is Element of A : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (x . i) where x is Element of A : verum  }  c=  {  (x . i) where x is Element of Bool M : x in SF  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (x . i) where x is Element of Bool M : x in SF  }  or q in  {  (x . i) where x is Element of A : verum  }  )
assume  q in  {  (x . i) where x is Element of Bool M : x in SF  }  ; ::_thesis: q in  {  (x . i) where x is Element of A : verum  }
then  ex x being Element of Bool M st
( q = x . i & x in SF ) ;
hence  q in  {  (x . i) where x is Element of A : verum  }  by A3; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (x . i) where x is Element of A : verum  }  or q in  {  (x . i) where x is Element of Bool M : x in SF  }  )
assume  q in  {  (x . i) where x is Element of A : verum  }  ; ::_thesis: q in  {  (x . i) where x is Element of Bool M : x in SF  }
then consider x being Element of A such that
A7: q = x . i ;
 x in SF by A3;
hence  q in  {  (x . i) where x is Element of Bool M : x in SF  }  by A7; ::_thesis: verum
end;
 |:SF:| = |.SF.| by A2, Def3;
hence  |:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }  by A4, A5, A1, A6; ::_thesis: verum
end;

registration
let I be set ;
let M be ManySortedSet of I;
let SF be non empty SubsetFamily of M;
cluster|:SF:| -> V8() ;
coherence
 |:SF:| is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not |:SF:| . i is empty )
assume  i in I ; ::_thesis: not |:SF:| . i is empty
then A1: |:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }  by Th14;
consider x being set  such that
A2: x in SF by XBOOLE_0:def_1;
reconsider x = x as Element of Bool M by A2;
 x . i in |:SF:| . i by A1, A2;
hence  not |:SF:| . i is empty ; ::_thesis: verum
end;
end;

theorem Th15: :: CLOSURE2:15
for f being Function holds dom |.{f}.| = dom f
proof
let f be Function; ::_thesis: dom |.{f}.| = dom f
consider A being non empty functional set  such that
A1: A = {f} and
A2: dom |.{f}.| = meet  {  (dom x) where x is Element of A : verum  }  and
 for i being set st i in dom |.{f}.| holds
|.{f}.| . i =  {  (x . i) where x is Element of A : verum  }  by Def2;
set m =  {  (dom x) where x is Element of A : verum  }  ;
  {  (dom x) where x is Element of A : verum  }  = {(dom f)}
proof
thus   {  (dom x) where x is Element of A : verum  }  c= {(dom f)} :: according to XBOOLE_0:def_10 ::_thesis: {(dom f)} c=  {  (dom x) where x is Element of A : verum  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (dom x) where x is Element of A : verum  }  or q in {(dom f)} )
assume  q in  {  (dom x) where x is Element of A : verum  }  ; ::_thesis: q in {(dom f)}
then consider x being Element of A such that
A3: q = dom x ;
 x = f by A1, TARSKI:def_1;
hence  q in {(dom f)} by A3, TARSKI:def_1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(dom f)} or q in  {  (dom x) where x is Element of A : verum  }  )
assume  q in {(dom f)} ; ::_thesis: q in  {  (dom x) where x is Element of A : verum  }
then A4: q = dom f by TARSKI:def_1;
 f is Element of A by A1, TARSKI:def_1;
hence  q in  {  (dom x) where x is Element of A : verum  }  by A4; ::_thesis: verum
end;
hence  dom |.{f}.| = dom f by A2, SETFAM_1:10; ::_thesis: verum
end;

theorem :: CLOSURE2:16
for f, f1 being Function holds dom |.{f,f1}.| = (dom f) /\ (dom f1)
proof
let f, f1 be Function; ::_thesis: dom |.{f,f1}.| = (dom f) /\ (dom f1)
consider A being non empty functional set  such that
A1: A = {f,f1} and
A2: dom |.{f,f1}.| = meet  {  (dom x) where x is Element of A : verum  }  and
 for i being set st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i =  {  (x . i) where x is Element of A : verum  }  by Def2;
set m =  {  (dom x) where x is Element of A : verum  }  ;
  {  (dom x) where x is Element of A : verum  }  = {(dom f),(dom f1)}
proof
thus   {  (dom x) where x is Element of A : verum  }  c= {(dom f),(dom f1)} :: according to XBOOLE_0:def_10 ::_thesis: {(dom f),(dom f1)} c=  {  (dom x) where x is Element of A : verum  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (dom x) where x is Element of A : verum  }  or q in {(dom f),(dom f1)} )
assume  q in  {  (dom x) where x is Element of A : verum  }  ; ::_thesis: q in {(dom f),(dom f1)}
then consider x being Element of A such that
A3: q = dom x ;
 ( x = f or x = f1 ) by A1, TARSKI:def_2;
hence  q in {(dom f),(dom f1)} by A3, TARSKI:def_2; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(dom f),(dom f1)} or q in  {  (dom x) where x is Element of A : verum  }  )
assume  q in {(dom f),(dom f1)} ; ::_thesis: q in  {  (dom x) where x is Element of A : verum  }
then A4: ( q = dom f or q = dom f1 ) by TARSKI:def_2;
 ( f is Element of A & f1 is Element of A ) by A1, TARSKI:def_2;
hence  q in  {  (dom x) where x is Element of A : verum  }  by A4; ::_thesis: verum
end;
hence  dom |.{f,f1}.| = (dom f) /\ (dom f1) by A2, SETFAM_1:11; ::_thesis: verum
end;

theorem Th17: :: CLOSURE2:17
for i being set
for f being Function st i in dom f holds
|.{f}.| . i = {(f . i)}
proof
let i be set ; ::_thesis: for f being Function st i in dom f holds
|.{f}.| . i = {(f . i)}
let f be Function; ::_thesis: ( i in dom f implies |.{f}.| . i = {(f . i)} )
A1: f in {f} by TARSKI:def_1;
consider A being non empty functional set  such that
A2: A = {f} and
 dom |.{f}.| = meet  {  (dom x) where x is Element of A : verum  }  and
A3: for i being set st i in dom |.{f}.| holds
|.{f}.| . i =  {  (x . i) where x is Element of A : verum  }  by Def2;
assume  i in dom f ; ::_thesis: |.{f}.| . i = {(f . i)}
then  i in dom |.{f}.| by Th15;
then A4: |.{f}.| . i =  {  (x . i) where x is Element of A : verum  }  by A3;
thus  |.{f}.| . i c= {(f . i)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . i)} c= |.{f}.| . i
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in |.{f}.| . i or q in {(f . i)} )
assume  q in |.{f}.| . i ; ::_thesis: q in {(f . i)}
then consider x being Element of A such that
A5: q = x . i by A4;
 x = f by A2, TARSKI:def_1;
hence  q in {(f . i)} by A5, TARSKI:def_1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(f . i)} or q in |.{f}.| . i )
assume  q in {(f . i)} ; ::_thesis: q in |.{f}.| . i
then  q = f . i by TARSKI:def_1;
hence  q in |.{f}.| . i by A2, A4, A1; ::_thesis: verum
end;

theorem :: CLOSURE2:18
for i, I being set
for M being ManySortedSet of I
for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
proof
let i, I be set ; ::_thesis: for M being ManySortedSet of I
for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let M be ManySortedSet of I; ::_thesis: for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let f be Function; ::_thesis: for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let SF be SubsetFamily of M; ::_thesis: ( i in I & SF = {f} implies |:SF:| . i = {(f . i)} )
assume that
A1: i in I and
A2: SF = {f} ; ::_thesis: |:SF:| . i = {(f . i)}
A3: |:SF:| = |.SF.| by A2, Def3;
 dom |:SF:| = I by PARTFUN1:def_2;
then  i in dom f by A1, A2, A3, Th15;
hence  |:SF:| . i = {(f . i)} by A2, A3, Th17; ::_thesis: verum
end;

theorem Th19: :: CLOSURE2:19
for i being set
for f, f1 being Function st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = {(f . i),(f1 . i)}
proof
let i be set ; ::_thesis: for f, f1 being Function st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = {(f . i),(f1 . i)}
let f, f1 be Function; ::_thesis: ( i in dom |.{f,f1}.| implies |.{f,f1}.| . i = {(f . i),(f1 . i)} )
A1: ( f in {f,f1} & f1 in {f,f1} ) by TARSKI:def_2;
consider A being non empty functional set  such that
A2: A = {f,f1} and
 dom |.{f,f1}.| = meet  {  (dom x) where x is Element of A : verum  }  and
A3: for i being set st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i =  {  (x . i) where x is Element of A : verum  }  by Def2;
assume  i in dom |.{f,f1}.| ; ::_thesis: |.{f,f1}.| . i = {(f . i),(f1 . i)}
then A4: |.{f,f1}.| . i =  {  (x . i) where x is Element of A : verum  }  by A3;
thus  |.{f,f1}.| . i c= {(f . i),(f1 . i)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . i),(f1 . i)} c= |.{f,f1}.| . i
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in |.{f,f1}.| . i or q in {(f . i),(f1 . i)} )
assume  q in |.{f,f1}.| . i ; ::_thesis: q in {(f . i),(f1 . i)}
then consider x being Element of A such that
A5: q = x . i by A4;
percases ( x = f or x = f1 ) by A2, TARSKI:def_2;
suppose x = f ; ::_thesis: q in {(f . i),(f1 . i)}
hence  q in {(f . i),(f1 . i)} by A5, TARSKI:def_2; ::_thesis: verum
end;
suppose x = f1 ; ::_thesis: q in {(f . i),(f1 . i)}
hence  q in {(f . i),(f1 . i)} by A5, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(f . i),(f1 . i)} or q in |.{f,f1}.| . i )
assume  q in {(f . i),(f1 . i)} ; ::_thesis: q in |.{f,f1}.| . i
then  ( q = f . i or q = f1 . i ) by TARSKI:def_2;
hence  q in |.{f,f1}.| . i by A2, A4, A1; ::_thesis: verum
end;

theorem Th20: :: CLOSURE2:20
for i, I being set
for M being ManySortedSet of I
for f, f1 being Function
for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
proof
let i, I be set ; ::_thesis: for M being ManySortedSet of I
for f, f1 being Function
for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
let M be ManySortedSet of I; ::_thesis: for f, f1 being Function
for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
let f, f1 be Function; ::_thesis: for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}
let SF be SubsetFamily of M; ::_thesis: ( i in I & SF = {f,f1} implies |:SF:| . i = {(f . i),(f1 . i)} )
assume that
A1: i in I and
A2: SF = {f,f1} ; ::_thesis: |:SF:| . i = {(f . i),(f1 . i)}
 ( dom |:SF:| = I & |:SF:| = |.SF.| ) by A2, Def3, PARTFUN1:def_2;
hence  |:SF:| . i = {(f . i),(f1 . i)} by A1, A2, Th19; ::_thesis: verum
end;

definition
let I be set ;
let M be ManySortedSet of I;
let SF be SubsetFamily of M;
:: original: |:
redefine func|:SF:| ->  MSSubsetFamily of M;
coherence
 |:SF:| is MSSubsetFamily of M
proof
percases ( not SF is empty or SF is empty ) ;
supposeA1: not SF is empty ; ::_thesis: |:SF:| is MSSubsetFamily of M
 |: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 A2: i in I ; ::_thesis: |:SF:| . i c= (bool M) . i
then A3: |:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }  by A1, Th14;
thus  |:SF:| . i c= (bool M) . i ::_thesis: verum
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 consider a being Element of Bool M such that
A4: x = a . i and
 a in SF by A3;
 a c= M by PBOOLE:def_18;
then  x c= M . i by A2, A4, PBOOLE:def_2;
then  x in bool (M . i) ;
hence  x in (bool M) . i by A2, MBOOLEAN:def_1; ::_thesis: verum
end;
end;
hence  |:SF:| is MSSubsetFamily of M ; ::_thesis: verum
end;
suppose SF is empty ; ::_thesis: |:SF:| is MSSubsetFamily of M
then  |:SF:| = [[0]] I by Def3;
hence  |:SF:| is MSSubsetFamily of M by MSSUBFAM:31; ::_thesis: verum
end;
end;
end;
end;

theorem Th21: :: CLOSURE2:21
for I being set
for M, A being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
proof
let I be set ; ::_thesis: for M, A being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
let M, A be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
let SF be SubsetFamily of M; ::_thesis: ( A in SF implies A in' |:SF:| )
assume A1: A in SF ; ::_thesis: A in' |:SF:|
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in |:SF:| . i )
assume  i in I ; ::_thesis: A . i in |:SF:| . i
then  |:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }  by A1, Th14;
hence  A . i in |:SF:| . i by A1; ::_thesis: verum
end;

theorem Th22: :: CLOSURE2:22
for I being set
for M, A, B being ManySortedSet of I
for SF being SubsetFamily of M st SF = {A,B} holds
union |:SF:| = A \/ B
proof
let I be set ; ::_thesis: for M, A, B being ManySortedSet of I
for SF being SubsetFamily of M st SF = {A,B} holds
union |:SF:| = A \/ B
let M, A, B be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M st SF = {A,B} holds
union |:SF:| = A \/ B
let SF be SubsetFamily of M; ::_thesis: ( SF = {A,B} implies union |:SF:| = A \/ B )
assume A1: SF = {A,B} ; ::_thesis: union |:SF:| = A \/ B
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_|:SF:|)_._i_=_(A_\/_B)_._i
let i be set ; ::_thesis: ( i in I implies (union |:SF:|) . i = (A \/ B) . i )
assume A2: i in I ; ::_thesis: (union |:SF:|) . i = (A \/ B) . i
hence (union |:SF:|) . i = union (|:SF:| . i) by MBOOLEAN:def_2
.= union {(A . i),(B . i)} by A1, A2, Th20
.= (A . i) \/ (B . i) by ZFMISC_1:75
.= (A \/ B) . i by A2, PBOOLE:def_4 ;
::_thesis: verum
end;
hence  union |:SF:| = A \/ B by PBOOLE:3; ::_thesis: verum
end;

theorem Th23: :: CLOSURE2:23
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
let M be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
let SF be SubsetFamily of M; ::_thesis: for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E /\ T
let E, T be Element of Bool M; ::_thesis: ( SF = {E,T} implies meet |:SF:| = E /\ T )
assume A1: SF = {E,T} ; ::_thesis: meet |:SF:| = E /\ T
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(meet_|:SF:|)_._i_=_(E_/\_T)_._i
reconsider sf1 = SF as non empty SubsetFamily of M by A1;
let i be set ; ::_thesis: ( i in I implies (meet |:SF:|) . i = (E /\ T) . i )
assume A2: i in I ; ::_thesis: (meet |:SF:|) . i = (E /\ T) . i
 ex Q being Subset-Family of (M . i) st
( Q = |:sf1:| . i & (meet |:sf1:|) . i = Intersect Q ) by A2, MSSUBFAM:def_1;
hence (meet |:SF:|) . i = meet (|:sf1:| . i) by A2, SETFAM_1:def_9
.= meet {(E . i),(T . i)} by A1, A2, Th20
.= (E . i) /\ (T . i) by SETFAM_1:11
.= (E /\ T) . i by A2, PBOOLE:def_5 ;
::_thesis: verum
end;
hence  meet |:SF:| = E /\ T by PBOOLE:3; ::_thesis: verum
end;

theorem Th24: :: CLOSURE2:24
for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let M be ManySortedSet of I; ::_thesis: for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let SF be SubsetFamily of M; ::_thesis: for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let Z be ManySortedSubset of M; ::_thesis: ( ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) implies Z c=' meet |:SF:| )
assume A1: for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ; ::_thesis: Z c=' meet |:SF:|
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or Z . i c= (meet |:SF:|) . i )
assume A2: i in I ; ::_thesis: Z . i c= (meet |:SF:|) . i
consider Q being Subset-Family of (M . i) such that
A3: Q = |:SF:| . i and
A4: (meet |:SF:|) . i = Intersect Q by A2, MSSUBFAM:def_1;
A5: now__::_thesis:_for_q_being_set_st_q_in_Q_holds_
Z_._i_c=_q
let q be set ; ::_thesis: ( q in Q implies Z . i c= b1 )
assume A6: q in Q ; ::_thesis: Z . i c= b1
percases ( not SF is empty or SF is empty ) ;
suppose not SF is empty ; ::_thesis: Z . i c= b1
then  |:SF:| . i =  {  (x . i) where x is Element of Bool M : x in SF  }  by A2, Th14;
then consider a being Element of Bool M such that
A7: q = a . i and
A8: a in SF by A3, A6;
 Z c=' a by A1, A8;
hence  Z . i c= q by A2, A7, PBOOLE:def_2; ::_thesis: verum
end;
suppose SF is empty ; ::_thesis: Z . i c= b1
then  |:SF:| = [[0]] I by Def3;
hence  Z . i c= q by A3, A6; ::_thesis: verum
end;
end;
end;
 Z c= M by PBOOLE:def_18;
then  Z . i is Subset of (M . i) by A2, PBOOLE:def_2;
hence  Z . i c= (meet |:SF:|) . i by A4, A5, MSSUBFAM:4; ::_thesis: verum
end;

theorem :: CLOSURE2:25
for I being set
for M being ManySortedSet of I holds |:(Bool M):| = bool M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I holds |:(Bool M):| = bool M
let M be ManySortedSet of I; ::_thesis: |:(Bool M):| = bool M
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
|:(Bool_M):|_._i_=_(bool_M)_._i
let i be set ; ::_thesis: ( i in I implies |:(Bool M):| . i = (bool M) . i )
assume A1: i in I ; ::_thesis: |:(Bool M):| . i = (bool M) . i
then A2: |:(Bool M):| . i =  {  (x . i) where x is Element of Bool M : x in Bool M  }  by Th14;
thus  |:(Bool M):| . i = (bool M) . i ::_thesis: verum
proof
thus  |:(Bool M):| . i c= (bool M) . i :: according to XBOOLE_0:def_10 ::_thesis: (bool M) . i c= |:(Bool M):| . i
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in |:(Bool M):| . i or q in (bool M) . i )
assume  q in |:(Bool M):| . i ; ::_thesis: q in (bool M) . i
then consider x being Element of Bool M such that
A3: q = x . i and
 x in Bool M by A2;
 x c= M by PBOOLE:def_18;
then  x . i c= M . i by A1, PBOOLE:def_2;
then  x . i in bool (M . i) ;
hence  q in (bool M) . i by A1, A3, MBOOLEAN:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (bool M) . i or a in |:(Bool M):| . i )
assume A4: a in (bool M) . i ; ::_thesis: a in |:(Bool M):| . i
 dom (([[0]] I) +* (i .--> a)) = I by A1, PZFMISC1:1;
then reconsider X = ([[0]] I) +* (i .--> a) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> a) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A6: X . i = (i .--> a) . i by A5, FUNCT_4:13
.= a by FUNCOP_1:72 ;
 X is ManySortedSubset of M
proof
let s be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not s in I or X . s c= M . s )
assume A7: s in I ; ::_thesis: X . s c= M . s
percases ( s = i or s <> i ) ;
supposeA8: s = i ; ::_thesis: X . s c= M . s
then  a in bool (M . s) by A4, A7, MBOOLEAN:def_1;
hence  X . s c= M . s by A6, A8; ::_thesis: verum
end;
suppose s <> i ; ::_thesis: X . s c= M . s
then  not s in dom (i .--> a) by A5, TARSKI:def_1;
then X . s = ([[0]] I) . s by FUNCT_4:11
.= {} ;
hence  X . s c= M . s by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
then  X is Element of Bool M by Def1;
hence  a in |:(Bool M):| . i by A2, A6; ::_thesis: verum
end;
end;
hence  |:(Bool M):| = bool M by PBOOLE:3; ::_thesis: verum
end;

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

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

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

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

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

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

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

Lm1:  for I being set
for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let I be set ; ::_thesis: for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
let M be ManySortedSet of I; ::_thesis: ( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
thus  Bool M is additive ::_thesis: ( Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let A be ManySortedSet of I; :: according to CLOSURE2:def_4 ::_thesis: for B being ManySortedSet of I st A in Bool M & B in Bool M holds
A \/ B in Bool M
let B be ManySortedSet of I; ::_thesis: ( A in Bool M & B in Bool M implies A \/ B in Bool M )
assume  ( A in Bool M & B in Bool M ) ; ::_thesis: A \/ B in Bool M
hence  A \/ B in Bool M by Th10; ::_thesis: verum
end;
thus  Bool M is absolutely-additive ::_thesis: ( Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let F be SubsetFamily of M; :: according to CLOSURE2:def_5 ::_thesis: ( F c= Bool M implies union |:F:| in Bool M )
assume  F c= Bool M ; ::_thesis: union |:F:| in Bool M
 union |:F:| c= M by MSSUBFAM:40;
then  union |:F:| is ManySortedSubset of M by PBOOLE:def_18;
hence  union |:F:| in Bool M by Def1; ::_thesis: verum
end;
thus  Bool M is multiplicative ::_thesis: ( Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let A be ManySortedSet of I; :: according to CLOSURE2:def_6 ::_thesis: for B being ManySortedSet of I st A in Bool M & B in Bool M holds
A /\ B in Bool M
let B be ManySortedSet of I; ::_thesis: ( A in Bool M & B in Bool M implies A /\ B in Bool M )
assume  ( A in Bool M & B in Bool M ) ; ::_thesis: A /\ B in Bool M
hence  A /\ B in Bool M by Th9; ::_thesis: verum
end;
thus  Bool M is absolutely-multiplicative ::_thesis: ( Bool M is properly-upper-bound & Bool M is properly-lower-bound )
proof
let F be SubsetFamily of M; :: according to CLOSURE2:def_7 ::_thesis: ( F c= Bool M implies meet |:F:| in Bool M )
assume  F c= Bool M ; ::_thesis: meet |:F:| in Bool M
thus  meet |:F:| in Bool M by Def1; ::_thesis: verum
end;
 M is ManySortedSubset of M by PBOOLE:def_18;
then  M in Bool M by Def1;
hence  Bool M is properly-upper-bound by Def8; ::_thesis: Bool M is properly-lower-bound
 [[0]] I c= M by PBOOLE:43;
then  [[0]] I is ManySortedSubset of M by PBOOLE:def_18;
hence  [[0]] I in Bool M by Def1; :: according to CLOSURE2:def_9 ::_thesis: verum
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for Element of bool (Bool M);
existence
 ex b1 being SubsetFamily of M st
( not b1 is empty & b1 is functional & b1 is with_common_domain & 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
take  Bool M ; ::_thesis: ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain & Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
thus  ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain & Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound ) by Lm1; ::_thesis: verum
end;
end;

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

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive  ->  additive for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is absolutely-additive holds
b1 is additive
proof
let SF be SubsetFamily of M; ::_thesis: ( SF is absolutely-additive implies SF is additive )
assume A1: SF is absolutely-additive ; ::_thesis: SF is additive
let A be ManySortedSet of I; :: according to CLOSURE2:def_4 ::_thesis: for B being ManySortedSet of I st A in SF & B in SF holds
A \/ B in SF
let B be ManySortedSet of I; ::_thesis: ( A in SF & B in SF implies A \/ B in SF )
assume that
A2: A in SF and
A3: B in SF ; ::_thesis: A \/ B in SF
 B is ManySortedSubset of M by A3, Def1;
then A4: B c= M by PBOOLE:def_18;
 A is ManySortedSubset of M by A2, Def1;
then  A c= M by PBOOLE:def_18;
then reconsider ab = {A,B} as SubsetFamily of M by A4, Th8;
 ( {A} c= SF & {B} c= SF ) by A2, A3, ZFMISC_1:31;
then  {A} \/ {B} c= SF by XBOOLE_1:8;
then  {A,B} c= SF by ENUMSET1:1;
then  union |:ab:| in SF by A1, Def5;
hence  A \/ B in SF by Th22; ::_thesis: verum
end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative  ->  multiplicative for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is multiplicative
proof
let SF be SubsetFamily of M; ::_thesis: ( SF is absolutely-multiplicative implies SF is multiplicative )
assume A1: SF is absolutely-multiplicative ; ::_thesis: SF is multiplicative
let A be ManySortedSet of I; :: according to CLOSURE2:def_6 ::_thesis: for B being ManySortedSet of I st A in SF & B in SF holds
A /\ B in SF
let B be ManySortedSet of I; ::_thesis: ( A in SF & B in SF implies A /\ B in SF )
assume that
A2: A in SF and
A3: B in SF ; ::_thesis: A /\ B in SF
 B is ManySortedSubset of M by A3, Def1;
then A4: B c= M by PBOOLE:def_18;
 A is ManySortedSubset of M by A2, Def1;
then  A c= M by PBOOLE:def_18;
then reconsider ab = {A,B} as SubsetFamily of M by A4, Th8;
 ( {A} c= SF & {B} c= SF ) by A2, A3, ZFMISC_1:31;
then  {A} \/ {B} c= SF by XBOOLE_1:8;
then  {A,B} c= SF by ENUMSET1:1;
then  meet |:ab:| in SF by A1, Def7;
hence  A /\ B in SF by A2, A3, Th23; ::_thesis: verum
end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative  ->  properly-upper-bound for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proof
reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
let SF be SubsetFamily of M; ::_thesis: ( SF is absolutely-multiplicative implies SF is properly-upper-bound )
assume A1: SF is absolutely-multiplicative ; ::_thesis: SF is properly-upper-bound
 |:a:| = [[0]] I by Def3;
then A2: meet |:a:| = M by MSSUBFAM:41;
 a c= SF by XBOOLE_1:2;
hence  M in SF by A1, A2, Def7; :: according to CLOSURE2:def_8 ::_thesis: verum
end;
end;

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

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive  ->  properly-lower-bound for Element of bool (Bool M);
coherence
 for b1 being SubsetFamily of M st b1 is absolutely-additive holds
b1 is properly-lower-bound
proof
reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
let SF be SubsetFamily of M; ::_thesis: ( SF is absolutely-additive implies SF is properly-lower-bound )
assume A1: SF is absolutely-additive ; ::_thesis: SF is properly-lower-bound
 |:a:| = [[0]] I by Def3;
then A2: union |:a:| = [[0]] I by MBOOLEAN:21;
 a c= SF by XBOOLE_1:2;
hence  [[0]] I in SF by A1, A2, Def5; :: according to CLOSURE2:def_9 ::_thesis: verum
end;
end;

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

begin

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

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

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

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

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

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

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

registration
let I be set ;
let M be ManySortedSet of I;
cluster non empty Relation-like Function-like V17( Bool M) quasi_total reflexive monotonic idempotent topological for Element of bool [:(Bool M),(Bool M):];
existence
 ex b1 being SetOp of M st
( b1 is reflexive & b1 is monotonic & b1 is idempotent & b1 is topological )
proof
reconsider f = id (Bool M) as SetOp 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 CLOSURE2:def_10 ::_thesis: X c=' f . X
thus  X c=' f . X by FUNCT_1:18; ::_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 CLOSURE2:def_11 ::_thesis: ( X c=' Y implies f . X c=' f . Y )
assume A1: X c= Y ; ::_thesis: f . X c=' f . Y
 f . X = X by FUNCT_1:18;
hence  f . X c=' f . Y by A1, FUNCT_1:18; ::_thesis: verum
end;
thus  f is idempotent ::_thesis: f is topological
proof
let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: f . X = f . (f . X)
thus  f . (f . X) = f . X by FUNCT_1:18; ::_thesis: verum
end;
thus  f is topological ::_thesis: verum
proof
let X, Y be Element of Bool M; :: according to CLOSURE2:def_13 ::_thesis: f . (X \/ Y) = (f . X) \/ (f . Y)
 ( X c= M & Y c= M ) by PBOOLE:def_18;
then  X \/ Y c= M by PBOOLE:16;
then  X \/ Y is ManySortedSubset of M by PBOOLE:def_18;
then  X \/ Y in Bool M by Def1;
hence f . (X \/ Y) = X \/ Y by FUNCT_1:18
.= (f . X) \/ Y by FUNCT_1:18
.= (f . X) \/ (f . Y) by FUNCT_1:18 ;
::_thesis: verum
end;
end;
end;

theorem :: CLOSURE2:26
for I being set
for A being ManySortedSet of I holds id (Bool A) is reflexive SetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (Bool A) is reflexive SetOp of A
let A be ManySortedSet of I; ::_thesis: id (Bool A) is reflexive SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
 f is reflexive
proof
let X be Element of Bool A; :: according to CLOSURE2:def_10 ::_thesis: X c=' f . X
thus  X c=' f . X by FUNCT_1:18; ::_thesis: verum
end;
hence  id (Bool A) is reflexive SetOp of A ; ::_thesis: verum
end;

theorem :: CLOSURE2:27
for I being set
for A being ManySortedSet of I holds id (Bool A) is monotonic SetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (Bool A) is monotonic SetOp of A
let A be ManySortedSet of I; ::_thesis: id (Bool A) is monotonic SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
 f is monotonic
proof
let X, Y be Element of Bool A; :: according to CLOSURE2:def_11 ::_thesis: ( X c=' Y implies f . X c=' f . Y )
assume A1: X c= Y ; ::_thesis: f . X c=' f . Y
 f . X = X by FUNCT_1:18;
hence  f . X c=' f . Y by A1, FUNCT_1:18; ::_thesis: verum
end;
hence  id (Bool A) is monotonic SetOp of A ; ::_thesis: verum
end;

theorem :: CLOSURE2:28
for I being set
for A being ManySortedSet of I holds id (Bool A) is idempotent SetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (Bool A) is idempotent SetOp of A
let A be ManySortedSet of I; ::_thesis: id (Bool A) is idempotent SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
 f is idempotent
proof
let X be Element of Bool A; :: according to CLOSURE2:def_12 ::_thesis: f . X = f . (f . X)
thus  f . (f . X) = f . X by FUNCT_1:18; ::_thesis: verum
end;
hence  id (Bool A) is idempotent SetOp of A ; ::_thesis: verum
end;

theorem :: CLOSURE2:29
for I being set
for A being ManySortedSet of I holds id (Bool A) is topological SetOp of A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds id (Bool A) is topological SetOp of A
let A be ManySortedSet of I; ::_thesis: id (Bool A) is topological SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
 f is topological
proof
let X, Y be Element of Bool A; :: according to CLOSURE2:def_13 ::_thesis: f . (X \/ Y) = (f . X) \/ (f . Y)
 ( X c= A & Y c= A ) by PBOOLE:def_18;
then  X \/ Y c= A by PBOOLE:16;
then  X \/ Y is ManySortedSubset of A by PBOOLE:def_18;
then  X \/ Y in Bool A by Def1;
hence f . (X \/ Y) = X \/ Y by FUNCT_1:18
.= (f . X) \/ Y by FUNCT_1:18
.= (f . X) \/ (f . Y) by FUNCT_1:18 ;
::_thesis: verum
end;
hence  id (Bool A) is topological SetOp of A ; ::_thesis: verum
end;


theorem :: CLOSURE2:30
for I being set
for M being ManySortedSet of I
for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let M be ManySortedSet of I; ::_thesis: for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let E be Element of Bool M; ::_thesis: for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let g be SetOp of M; ::_thesis: ( E = M & g is reflexive implies E = g . E )
assume A1: E = M ; ::_thesis: ( not g is reflexive or E = g . E )
assume  g is reflexive ; ::_thesis: E = g . E
then A2: E c= g . E by Def10;
 g . E c= E by A1, PBOOLE:def_18;
hence  E = g . E by A2, PBOOLE:146; ::_thesis: verum
end;

theorem :: CLOSURE2:31
for I being set
for M being ManySortedSet of I
for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
let M be ManySortedSet of I; ::_thesis: for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
let g be SetOp of M; ::_thesis: ( g is reflexive & ( for X being Element of Bool M holds g . X c= X ) implies g is idempotent )
assume that
A1: g is reflexive and
A2: for X being Element of Bool M holds g . X c= X ; ::_thesis: g is idempotent
let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: g . X = g . (g . X)
A3: g . X c= g . (g . X) by A1, Def10;
 g . (g . X) c= g . X by A2;
hence  g . X = g . (g . X) by A3, PBOOLE:146; ::_thesis: verum
end;

theorem :: CLOSURE2:32
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
let E, T be Element of Bool M; ::_thesis: for g being SetOp of M
for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
let g be SetOp of M; ::_thesis: for A being Element of Bool M st A = E /\ T & g is monotonic holds
g . A c= (g . E) /\ (g . T)
let A be Element of Bool M; ::_thesis: ( A = E /\ T & g is monotonic implies g . A c= (g . E) /\ (g . T) )
assume A1: A = E /\ T ; ::_thesis: ( not g is monotonic or g . A c= (g . E) /\ (g . T) )
assume A2: g is monotonic ; ::_thesis: g . A c= (g . E) /\ (g . T)
 E /\ T c= T by PBOOLE:15;
then A3: g . A c= g . T by A1, A2, Def11;
 E /\ T c= E by PBOOLE:15;
then  g . A c= g . E by A1, A2, Def11;
hence  g . A c= (g . E) /\ (g . T) by A3, PBOOLE:17; ::_thesis: verum
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster Function-like quasi_total topological  ->  monotonic for Element of bool [:(Bool M),(Bool M):];
coherence
 for b1 being SetOp of M st b1 is topological holds
b1 is monotonic
proof
let g be SetOp of M; ::_thesis: ( g is topological implies g is monotonic )
assume A1: g is topological ; ::_thesis: g is monotonic
let X, Y be Element of Bool M; :: according to CLOSURE2:def_11 ::_thesis: ( X c=' Y implies g . X c=' g . Y )
assume A2: X c= Y ; ::_thesis: g . X c=' g . Y
(g . X) \/ (g . Y) = g . (X \/ Y) by A1, Def13
.= g . Y by A2, PBOOLE:22 ;
hence  g . X c=' g . Y by PBOOLE:26; ::_thesis: verum
end;
end;

theorem :: CLOSURE2:33
for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
let M be ManySortedSet of I; ::_thesis: for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
let E, T be Element of Bool M; ::_thesis: for g being SetOp of M
for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
let g be SetOp of M; ::_thesis: for A being Element of Bool M st A = E \ T & g is topological holds
(g . E) \ (g . T) c= g . A
let A be Element of Bool M; ::_thesis: ( A = E \ T & g is topological implies (g . E) \ (g . T) c= g . A )
assume A1: A = E \ T ; ::_thesis: ( not g is topological or (g . E) \ (g . T) c= g . A )
assume A2: g is topological ; ::_thesis: (g . E) \ (g . T) c= g . A
then (g . E) \/ (g . T) = g . (E \/ T) by Def13
.= g . ((E \ T) \/ T) by PBOOLE:67
.= (g . A) \/ (g . T) by A1, A2, Def13 ;
then  g . E c= (g . A) \/ (g . T) by PBOOLE:14;
then  (g . E) \ (g . T) c= ((g . A) \/ (g . T)) \ (g . T) by PBOOLE:53;
then A3: (g . E) \ (g . T) c= (g . A) \ (g . T) by PBOOLE:75;
 (g . A) \ (g . T) c= g . A by PBOOLE:56;
hence  (g . E) \ (g . T) c= g . A by A3, PBOOLE:13; ::_thesis: verum
end;

definition
let I be set ;
let M be ManySortedSet of I;
let h, g be SetOp of M;
:: original: *
redefine funcg * h ->  SetOp of M;
coherence
 h * g is SetOp of M
proof
 g * h is Function of (Bool M),(Bool M) ;
hence  h * g is SetOp of M ; ::_thesis: verum
end;
end;

theorem :: CLOSURE2:34
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
let M be ManySortedSet of I; ::_thesis: for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
let g, h be SetOp of M; ::_thesis: ( g is reflexive & h is reflexive implies g * h is reflexive )
assume A1: ( g is reflexive & h is reflexive ) ; ::_thesis: g * h is reflexive
let X be Element of Bool M; :: according to CLOSURE2:def_10 ::_thesis: X c=' (g * h) . X
 ( X c= h . X & h . X c= g . (h . X) ) by A1, Def10;
then  ( dom h = Bool M & X c= g . (h . X) ) by FUNCT_2:def_1, PBOOLE:13;
hence  X c=' (g * h) . X by FUNCT_1:13; ::_thesis: verum
end;

theorem :: CLOSURE2:35
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic
let M be ManySortedSet of I; ::_thesis: for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic
let g, h be SetOp of M; ::_thesis: ( g is monotonic & h is monotonic implies g * h is monotonic )
assume that
A1: g is monotonic and
A2: h is monotonic ; ::_thesis: g * h is monotonic
A3: dom h = Bool M by FUNCT_2:def_1;
let X, Y be Element of Bool M; :: according to CLOSURE2:def_11 ::_thesis: ( X c=' Y implies (g * h) . X c=' (g * h) . Y )
assume  X c= Y ; ::_thesis: (g * h) . X c=' (g * h) . Y
then  h . X c= h . Y by A2, Def11;
then  g . (h . X) c= g . (h . Y) by A1, Def11;
then  g . (h . X) c= (g * h) . Y by A3, FUNCT_1:13;
hence  (g * h) . X c=' (g * h) . Y by A3, FUNCT_1:13; ::_thesis: verum
end;

theorem :: CLOSURE2:36
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent
let M be ManySortedSet of I; ::_thesis: for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent
let g, h be SetOp of M; ::_thesis: ( g is idempotent & h is idempotent & g * h = h * g implies g * h is idempotent )
assume that
A1: g is idempotent and
A2: h is idempotent and
A3: g * h = h * g ; ::_thesis: g * h is idempotent
let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: (g * h) . X = (g * h) . ((g * h) . X)
A4: dom g = Bool M by FUNCT_2:def_1;
A5: dom h = Bool M by FUNCT_2:def_1;
hence (g * h) . X = g . (h . X) by FUNCT_1:13
.= g . (h . (h . X)) by A2, Def12
.= g . (g . (h . (h . X))) by A1, Def12
.= g . ((h * g) . (h . X)) by A3, A5, FUNCT_1:13
.= g . (h . (g . (h . X))) by A4, FUNCT_1:13
.= g . (h . ((g * h) . X)) by A5, FUNCT_1:13
.= (g * h) . ((g * h) . X) by A5, FUNCT_1:13 ;
::_thesis: verum
end;

theorem :: CLOSURE2:37
for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological
let M be ManySortedSet of I; ::_thesis: for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological
let g, h be SetOp of M; ::_thesis: ( g is topological & h is topological implies g * h is topological )
assume that
A1: g is topological and
A2: h is topological ; ::_thesis: g * h is topological
let X, Y be Element of Bool M; :: according to CLOSURE2:def_13 ::_thesis: (g * h) . (X \/ Y) = ((g * h) . X) \/ ((g * h) . Y)
A3: dom h = Bool M by FUNCT_2:def_1;
hence (g * h) . (X \/ Y) = g . (h . (X \/ Y)) by Th10, FUNCT_1:13
.= g . ((h . X) \/ (h . Y)) by A2, Def13
.= (g . (h . X)) \/ (g . (h . Y)) by A1, Def13
.= ((g * h) . X) \/ (g . (h . Y)) by A3, FUNCT_1:13
.= ((g * h) . X) \/ ((g * h) . Y) by A3, FUNCT_1:13 ;
::_thesis: verum
end;

begin

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

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

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

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

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

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

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

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

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

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

registration
let S be 1-sorted ;
let MS be many-sorted over S;
cluster Full MS ->  strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence
 ( Full MS is strict & Full MS is additive & Full MS is absolutely-additive & Full MS is multiplicative & Full MS is absolutely-multiplicative & Full MS is properly-upper-bound & Full MS is properly-lower-bound )
proof
thus  Full MS is strict ; ::_thesis: ( Full MS is additive & Full MS is absolutely-additive & Full MS is multiplicative & Full MS is absolutely-multiplicative & Full MS is properly-upper-bound & Full MS is properly-lower-bound )
thus  ( the Family of (Full MS) is additive & the Family of (Full MS) is absolutely-additive & the Family of (Full MS) is multiplicative & the Family of (Full MS) is absolutely-multiplicative & the Family of (Full MS) is properly-upper-bound & the Family of (Full MS) is properly-lower-bound ) ; :: according to CLOSURE2:def_14,CLOSURE2:def_15,CLOSURE2:def_16,CLOSURE2:def_17,CLOSURE2:def_18,CLOSURE2:def_19 ::_thesis: verum
end;
end;

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

registration
let S be 1-sorted ;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ClosureStr over S;
existence
 ex b1 being ClosureStr over S st
( b1 is strict & 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  Full the non-empty many-sorted over S ; ::_thesis: ( Full the non-empty many-sorted over S is strict & Full the non-empty many-sorted over S is non-empty & Full the non-empty many-sorted over S is additive & Full the non-empty many-sorted over S is absolutely-additive & Full the non-empty many-sorted over S is multiplicative & Full the non-empty many-sorted over S is absolutely-multiplicative & Full the non-empty many-sorted over S is properly-upper-bound & Full the non-empty many-sorted over S is properly-lower-bound )
thus  ( Full the non-empty many-sorted over S is strict & Full the non-empty many-sorted over S is non-empty & Full the non-empty many-sorted over S is additive & Full the non-empty many-sorted over S is absolutely-additive & Full the non-empty many-sorted over S is multiplicative & Full the non-empty many-sorted over S is absolutely-multiplicative & Full the non-empty many-sorted over S is properly-upper-bound & Full 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 ClosureStr over S;
cluster the Family of CS ->  additive ;
coherence
 the Family of CS is additive by Def14;
end;

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

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

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

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

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

registration
let S be 1-sorted ;
let M be V8() ManySortedSet of the carrier of S;
let F be SubsetFamily of M;
cluster ClosureStr(# M,F #) ->  non-empty ;
coherence
 ClosureStr(# M,F #) is non-empty
proof
thus  the Sorts of ClosureStr(# 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 SubsetFamily of the Sorts of MS;
cluster ClosureStr(# the Sorts of MS,F #) ->  additive ;
coherence
 ClosureStr(# the Sorts of MS,F #) is additive by Def14;
end;

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

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

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

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

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

registration
let S be 1-sorted ;
cluster absolutely-additive  ->  additive for ClosureStr over S;
coherence
 for b1 being ClosureStr over S st b1 is absolutely-additive holds
b1 is additive
proof
let CS be ClosureStr 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 CLOSURE2:def_14 ::_thesis: verum
end;
end;

registration
let S be 1-sorted ;
cluster absolutely-multiplicative  ->  multiplicative for ClosureStr over S;
coherence
 for b1 being ClosureStr over S st b1 is absolutely-multiplicative holds
b1 is multiplicative
proof
let CS be ClosureStr 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 CLOSURE2:def_16 ::_thesis: verum
end;
end;

registration
let S be 1-sorted ;
cluster absolutely-multiplicative  ->  properly-upper-bound for ClosureStr over S;
coherence
 for b1 being ClosureStr over S st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proof
let CS be ClosureStr 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 CLOSURE2:def_18 ::_thesis: verum
end;
end;

registration
let S be 1-sorted ;
cluster absolutely-additive  ->  properly-lower-bound for ClosureStr over S;
coherence
 for b1 being ClosureStr over S st b1 is absolutely-additive holds
b1 is properly-lower-bound
proof
let CS be ClosureStr 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 CLOSURE2:def_19 ::_thesis: verum
end;
end;

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

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

definition
let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;
func ClOp->ClSys g ->  strict ClosureStr over S means :Def21: :: CLOSURE2:def 21
( the Sorts of it = A & the Family of it =  {  x where x is Element of Bool A : g . x = x  }  );
existence
 ex b1 being strict ClosureStr over S st
( the Sorts of b1 = A & the Family of b1 =  {  x where x is Element of Bool A : g . x = x  }  )
proof
defpred S1[ set ] means g . $1 = $1;
set SF =  {  x where x is Element of Bool A : S1[x]  }  ;
  {  x where x is Element of Bool A : S1[x]  }  is Subset of (Bool A) from DOMAIN_1:sch_7();
then reconsider D =  {  x where x is Element of Bool A : S1[x]  }  as SubsetFamily of A ;
take  ClosureStr(# A,D #) ; ::_thesis: ( the Sorts of ClosureStr(# A,D #) = A & the Family of ClosureStr(# A,D #) =  {  x where x is Element of Bool A : g . x = x  }  )
thus  ( the Sorts of ClosureStr(# A,D #) = A & the Family of ClosureStr(# A,D #) =  {  x where x is Element of Bool A : g . x = x  }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict ClosureStr over S st the Sorts of b1 = A & the Family of b1 =  {  x where x is Element of Bool A : g . x = x  }  & the Sorts of b2 = A & the Family of b2 =  {  x where x is Element of Bool A : g . x = x  }  holds
b1 = b2 ;
end;

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

registration
let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;
cluster ClOp->ClSys g ->  strict absolutely-multiplicative ;
coherence
 ClOp->ClSys g is absolutely-multiplicative
proof
A1: the Sorts of (ClOp->ClSys g) = A by Def21;
defpred S1[ set ] means g . S = S;
set SF =  {  x where x is Element of Bool A : S1[x]  }  ;
A2:  {  x where x is Element of Bool A : S1[x]  }  = the Family of (ClOp->ClSys g) by Def21;
  {  x where x is Element of Bool A : S1[x]  }  is Subset of (Bool A) from DOMAIN_1:sch_7();
then reconsider D =  {  x where x is Element of Bool A : S1[x]  }  as SubsetFamily of A ;
A3: ClOp->ClSys g = ClosureStr(# A,D #) by A1, A2;
 D is absolutely-multiplicative
proof
let F be SubsetFamily of A; :: according to CLOSURE2:def_7 ::_thesis: ( F c= D implies meet |:F:| in D )
assume A4: F c= D ; ::_thesis: meet |:F:| in D
reconsider mf = meet |:F:| as Element of Bool A by Def1;
now__::_thesis:_for_Z1_being_ManySortedSet_of_the_carrier_of_S_st_Z1_in_F_holds_
g_._mf_c='_Z1
let Z1 be ManySortedSet of the carrier of S; ::_thesis: ( Z1 in F implies g . mf c=' Z1 )
assume A5: Z1 in F ; ::_thesis: g . mf c=' Z1
then reconsider y1 = Z1 as Element of Bool A ;
 Z1 in D by A4, A5;
then A6: ex a being Element of Bool A st
( Z1 = a & g . a = a ) ;
 mf c=' y1 by A5, Th21, MSSUBFAM:43;
hence  g . mf c=' Z1 by A6, Def11; ::_thesis: verum
end;
then A7: g . mf c=' mf by Th24;
 mf c=' g . mf by Def10;
then  g . mf = mf by A7, PBOOLE:146;
hence  meet |:F:| in D ; ::_thesis: verum
end;
hence  ClOp->ClSys g is absolutely-multiplicative by A3; ::_thesis: verum
end;
end;

definition
let S be 1-sorted ;
let A be ClosureSystem of S;
let C be ManySortedSubset of the Sorts of A;
func Cl C ->  Element of Bool the Sorts of A means :Def22: :: CLOSURE2:def 22
 ex F being SubsetFamily of the Sorts of A st
( it = meet |:F:| & F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A )  }  );
existence
 ex b1 being Element of Bool the Sorts of A ex F being SubsetFamily of the Sorts of A st
( b1 = meet |:F:| & F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A )  }  )
proof
defpred S1[ Element of Bool the Sorts of A] means ( C c= $1 & $1 in the Family of A );
  {  X where X is Element of Bool the Sorts of A : S1[X]  }  is Subset of (Bool the Sorts of A) from DOMAIN_1:sch_7();
then reconsider F =  {  X where X is Element of Bool the Sorts of A : ( C c= X & X in the Family of A )  }  as SubsetFamily of the Sorts of A ;
reconsider IT = meet |:F:| as Element of Bool the Sorts of A by Def1;
take  IT ; ::_thesis: ex F being SubsetFamily of the Sorts of A st
( IT = meet |:F:| & F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A )  }  )
take  F ; ::_thesis: ( IT = meet |:F:| & F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A )  }  )
thus  ( IT = meet |:F:| & F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A )  }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of Bool the Sorts of A st ex F being SubsetFamily of the Sorts of A st
( b1 = meet |:F:| & F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A )  }  ) & ex F being SubsetFamily of the Sorts of A st
( b2 = meet |:F:| & F =  {  X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A )  }  ) holds
b1 = b2 ;
end;

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

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

theorem :: CLOSURE2:39
for S being 1-sorted
for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
proof
let S be 1-sorted ; ::_thesis: for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
deffunc H1( set ) ->  set = $1;
let D be ClosureSystem of S; ::_thesis: for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
let a be Element of Bool the Sorts of D; ::_thesis: for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
let f be SetOp of the Sorts of D; ::_thesis: ( f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) implies a in the Family of D )
assume A1: ( f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) ) ; ::_thesis: a in the Family of D
set F = the Family of D;
set M = the Sorts of D;
defpred S1[ Element of Bool the Sorts of D] means a c=' $1;
defpred S2[ Element of Bool the Sorts of D] means ( a c=' $1 & $1 in the Family of D );
defpred S3[ Element of Bool the Sorts of D] means ( $1 in the Family of D & a c=' $1 );
A2:  {  H1(w) where w is Element of Bool the Sorts of D : ( H1(w) in the Family of D & S1[w] )  }  c= the Family of D from FRAENKEL:sch_17();
A3: for q being Element of Bool the Sorts of D holds
( S2[q] iff S3[q] ) ;
A4:  {  H1(s) where s is Element of Bool the Sorts of D : S2[s]  }  =  {  H1(b) where b is Element of Bool the Sorts of D : S3[b]  }  from FRAENKEL:sch_3(A3);
consider SF being SubsetFamily of the Sorts of D such that
A5: Cl a = meet |:SF:| and
A6: SF =  {  X where X is Element of Bool the Sorts of D : ( a c= X & X in the Family of D )  }  by Def22;
 a = meet |:SF:| by A1, A5;
hence  a in the Family of D by A6, A2, A4, Def7; ::_thesis: verum
end;

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

definition
let S be 1-sorted ;
let D be ClosureSystem of S;
func ClSys->ClOp D ->  ClosureOperator of the Sorts of D means :Def23: :: CLOSURE2:def 23
 for x being Element of Bool the Sorts of D holds it . x = Cl x;
existence
 ex b1 being ClosureOperator of the Sorts of D st
for x being Element of Bool the Sorts of D holds b1 . x = Cl x
proof
set M = the Sorts of D;
deffunc H1( Element of Bool the Sorts of D) ->  Element of Bool the Sorts of D = Cl $1;
consider f being Function of (Bool the Sorts of D),(Bool the Sorts of D) such that
A1: for x being Element of Bool the Sorts of D holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider f = f as SetOp of the Sorts of D ;
reconsider f = f as ClosureOperator of the Sorts of D by A1, Th40;
take  f ; ::_thesis: for x being Element of Bool the Sorts of D holds f . x = Cl x
thus  for x being Element of Bool the Sorts of D holds f . x = Cl x by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ClosureOperator of the Sorts of D st ( for x being Element of Bool the Sorts of D holds b1 . x = Cl x ) & ( for x being Element of Bool the Sorts of D holds b2 . x = Cl x ) holds
b1 = b2
proof
let f, g be ClosureOperator of the Sorts of D; ::_thesis: ( ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) & ( for x being Element of Bool the Sorts of D holds g . x = Cl x ) implies f = g )
assume that
A2: for x being Element of Bool the Sorts of D holds f . x = Cl x and
A3: for x being Element of Bool the Sorts of D holds g . x = Cl x ; ::_thesis: f = g
now__::_thesis:_(_Bool_the_Sorts_of_D_=_dom_f_&_Bool_the_Sorts_of_D_=_dom_g_&_(_for_x_being_set_st_x_in_Bool_the_Sorts_of_D_holds_
f_._x_=_g_._x_)_)
set X = Bool the Sorts of D;
thus  Bool the Sorts of D = dom f by FUNCT_2:def_1; ::_thesis: ( Bool the Sorts of D = dom g & ( for x being set st x in Bool the Sorts of D holds
f . x = g . x ) )
thus  Bool the Sorts of D = dom g by FUNCT_2:def_1; ::_thesis: for x being set st x in Bool the Sorts of D holds
f . x = g . x
let x be set ; ::_thesis: ( x in Bool the Sorts of D implies f . x = g . x )
assume  x in Bool the Sorts of D ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of Bool the Sorts of D ;
thus f . x = Cl x1 by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence  f = g by FUNCT_1:2; ::_thesis: verum
end;
end;

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

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

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

theorem :: CLOSURE2:42
for S being 1-sorted
for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)
proof
let S be 1-sorted ; ::_thesis: for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)
let D be ClosureSystem of S; ::_thesis: ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)
set M = the Sorts of D;
set F = the Family of D;
set d = the Family of (ClOp->ClSys (ClSys->ClOp D));
set f = ClSys->ClOp D;
A1: the Family of (ClOp->ClSys (ClSys->ClOp D)) =  {  x where x is Element of Bool the Sorts of D : (ClSys->ClOp D) . x = x  }  by Def21;
 the Family of D = the Family of (ClOp->ClSys (ClSys->ClOp D))
proof
thus  the Family of D c= the Family of (ClOp->ClSys (ClSys->ClOp D)) :: according to XBOOLE_0:def_10 ::_thesis: the Family of (ClOp->ClSys (ClSys->ClOp D)) c= the Family of D
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the Family of D or q in the Family of (ClOp->ClSys (ClSys->ClOp D)) )
assume A2: q in the Family of D ; ::_thesis: q in the Family of (ClOp->ClSys (ClSys->ClOp D))
then reconsider q1 = q as Element of Bool the Sorts of D ;
consider SF being SubsetFamily of the Sorts of D such that
A3: Cl q1 = meet |:SF:| and
A4: SF =  {  X where X is Element of Bool the Sorts of D : ( q1 c= X & X in the Family of D )  }  by Def22;
 ( q1 c=' the Sorts of D & the Sorts of D in the Family of D ) by Def8, PBOOLE:def_18;
then  the Sorts of D in SF by A4;
then reconsider SF9 = SF as non empty SubsetFamily of the Sorts of D ;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
((ClSys->ClOp_D)_._q1)_._i_=_q1_._i
let i be set ; ::_thesis: ( i in the carrier of S implies ((ClSys->ClOp D) . q1) . i = q1 . i )
assume A5: i in the carrier of S ; ::_thesis: ((ClSys->ClOp D) . q1) . i = q1 . i
then consider Q being Subset-Family of ( the Sorts of D . i) such that
A6: Q = |:SF9:| . i and
A7: (meet |:SF9:|) . i = Intersect Q by MSSUBFAM:def_1;
A8: Q =  {  (x . i) where x is Element of Bool the Sorts of D : x in SF9  }  by A5, A6, Th14;
 q1 in SF9 by A2, A4;
then A9: q1 . i in Q by A8;
then A10: Intersect Q c= q1 . i by MSSUBFAM:2;
now__::_thesis:_for_z_being_set_st_z_in_Q_holds_
q1_._i_c=_z
let z be set ; ::_thesis: ( z in Q implies q1 . i c= z )
assume  z in Q ; ::_thesis: q1 . i c= z
then consider x being Element of Bool the Sorts of D such that
A11: z = x . i and
A12: x in SF9 by A8;
 ex xx being Element of Bool the Sorts of D st
( xx = x & q1 c=' xx & xx in the Family of D ) by A4, A12;
hence  q1 . i c= z by A5, A11, PBOOLE:def_2; ::_thesis: verum
end;
then  q1 . i c= Intersect Q by A9, MSSUBFAM:5;
then  Intersect Q = q1 . i by A10, XBOOLE_0:def_10;
hence  ((ClSys->ClOp D) . q1) . i = q1 . i by A3, A7, Def23; ::_thesis: verum
end;
then  (ClSys->ClOp D) . q1 = q1 by PBOOLE:3;
hence  q in the Family of (ClOp->ClSys (ClSys->ClOp D)) by A1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the Family of (ClOp->ClSys (ClSys->ClOp D)) or q in the Family of D )
assume  q in the Family of (ClOp->ClSys (ClSys->ClOp D)) ; ::_thesis: q in the Family of D
then consider x being Element of Bool the Sorts of D such that
A13: ( q = x & (ClSys->ClOp D) . x = x ) by A1;
defpred S1[ Element of Bool the Sorts of D] means ( $1 in the Family of D & x c=' $1 );
defpred S2[ Element of Bool the Sorts of D] means ( x c=' $1 & $1 in the Family of D );
defpred S3[ Element of Bool the Sorts of D] means x c=' $1;
A14:  {  H1(w) where w is Element of Bool the Sorts of D : ( H1(w) in the Family of D & S3[w] )  }  c= the Family of D from FRAENKEL:sch_17();
A15: for a being Element of Bool the Sorts of D holds
( S2[a] iff S1[a] ) ;
A16:  {  H1(a) where a is Element of Bool the Sorts of D : S2[a]  }  =  {  H1(b) where b is Element of Bool the Sorts of D : S1[b]  }  from FRAENKEL:sch_3(A15);
consider SF being SubsetFamily of the Sorts of D such that
A17: Cl x = meet |:SF:| and
A18: SF =  {  X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D )  }  by Def22;
 meet |:SF:| = q by A13, A17, Def23;
hence  q in the Family of D by A18, A14, A16, Def7; ::_thesis: verum
end;
hence  ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #) by Def21; ::_thesis: verum
end;