:: CLOSURE2 semantic presentation

notation
let c1 be set ;
let c2, c3 be ManySortedSet of c1;
synonym c2 in' c3 for c2 in c3;
end;

notation
let c1 be set ;
let c2, c3 be ManySortedSet of c1;
synonym c2 c=' c3 for c2 c= c3;
end;

theorem Th1: :: CLOSURE2:1
for b1 being non empty set
for b2, b3 being Element of b1 st b2 c= b3 holds
(id b1) . b2 c= (id b1) . b3
proof end;

theorem Th2: :: CLOSURE2:2
canceled;

theorem Th3: :: CLOSURE2:3
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3 being ManySortedSubset of b2 holds rng b3 c= union (rng (bool b2))
proof end;

registration
cluster empty -> functional set ;
coherence
for b1 being set st b1 is empty holds
b1 is functional
proof end;
end;

registration
cluster empty functional set ;
existence
ex b1 being set st
( b1 is empty & b1 is functional )
proof end;
end;

registration
let c1, c2 be Function;
cluster {a1,a2} -> functional ;
coherence
{c1,c2} is functional
proof end;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
defpred S1[ set ] means a1 is ManySortedSubset of c2;
func Bool c2 -> set means :Def1: :: CLOSURE2:def 1
for b1 being set holds
( b1 in a3 iff b1 is ManySortedSubset of a2 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is ManySortedSubset of c2 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is ManySortedSubset of c2 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is ManySortedSubset of c2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Bool CLOSURE2:def 1 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being set holds
( b3 = Bool b2 iff for b4 being set holds
( b4 in b3 iff b4 is ManySortedSubset of b2 ) );

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster Bool a2 -> non empty functional with_common_domain ;
coherence
( not Bool c2 is empty & Bool c2 is functional & Bool c2 is with_common_domain )
proof end;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
mode SubsetFamily of a2 is Subset of (Bool a2);
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
redefine func Bool as Bool c2 -> SubsetFamily of a2;
coherence
Bool c2 is SubsetFamily of c2
proof end;
end;

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster non empty functional with_common_domain Element of bool (Bool a2);
existence
ex b1 being SubsetFamily of c2 st
( not b1 is empty & b1 is functional & b1 is with_common_domain )
proof end;
end;

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster empty finite Element of bool (Bool a2);
existence
ex b1 being SubsetFamily of c2 st
( b1 is empty & b1 is finite )
proof end;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be non empty SubsetFamily of c2;
redefine mode Element as Element of c3 -> ManySortedSubset of a2;
coherence
for b1 being Element of c3 holds b1 is ManySortedSubset of c2
proof end;
end;

theorem Th4: :: CLOSURE2:4
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being SubsetFamily of b2 holds b3 \/ b4 is SubsetFamily of b2 ;

theorem Th5: :: CLOSURE2:5
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being SubsetFamily of b2 holds b3 /\ b4 is SubsetFamily of b2 ;

theorem Th6: :: CLOSURE2:6
for b1, b2 being set
for b3 being ManySortedSet of b1
for b4 being SubsetFamily of b3 holds b4 \ b2 is SubsetFamily of b3
proof end;

theorem Th7: :: CLOSURE2:7
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being SubsetFamily of b2 holds b3 \+\ b4 is SubsetFamily of b2 ;

theorem Th8: :: CLOSURE2:8
for b1 being set
for b2, b3 being ManySortedSet of b1 st b2 c= b3 holds
{b2} is SubsetFamily of b3
proof end;

theorem Th9: :: CLOSURE2:9
for b1 being set
for b2, b3, b4 being ManySortedSet of b1 st b2 c= b3 & b4 c= b3 holds
{b2,b4} is SubsetFamily of b3
proof end;

theorem Th10: :: CLOSURE2:10
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being Element of Bool b2 holds b3 /\ b4 in Bool b2
proof end;

theorem Th11: :: CLOSURE2:11
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being Element of Bool b2 holds b3 \/ b4 in Bool b2
proof end;

theorem Th12: :: CLOSURE2:12
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being Element of Bool b3 holds b4 \ b2 in Bool b3
proof end;

theorem Th13: :: CLOSURE2:13
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being Element of Bool b2 holds b3 \+\ b4 in Bool b2
proof end;

definition
let c1 be functional set ;
canceled;
func |.c1.| -> Function means :Def3: :: CLOSURE2:def 3
ex b1 being non empty functional set st
( b1 = a1 & dom a2 = meet { (dom b2) where B is Element of b1 : verum } & ( for b2 being set st b2 in dom a2 holds
a2 . b2 = { (b3 . b2) where B is Element of b1 : verum } ) ) if a1 <> {}
otherwise a2 = {} ;
existence
( ( c1 <> {} implies ex b1 being Functionex b2 being non empty functional set st
( b2 = c1 & dom b1 = meet { (dom b3) where B is Element of b2 : verum } & ( for b3 being set st b3 in dom b1 holds
b1 . b3 = { (b4 . b3) where B is Element of b2 : verum } ) ) ) & ( not c1 <> {} implies ex b1 being Function st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being Function holds
( ( c1 <> {} & ex b3 being non empty functional set st
( b3 = c1 & dom b1 = meet { (dom b4) where B is Element of b3 : verum } & ( for b4 being set st b4 in dom b1 holds
b1 . b4 = { (b5 . b4) where B is Element of b3 : verum } ) ) & ex b3 being non empty functional set st
( b3 = c1 & dom b2 = meet { (dom b4) where B is Element of b3 : verum } & ( for b4 being set st b4 in dom b2 holds
b2 . b4 = { (b5 . b4) where B is Element of b3 : verum } ) ) implies b1 = b2 ) & ( not c1 <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being Function holds verum ;
end;

:: deftheorem Def2 CLOSURE2:def 2 :
canceled;

:: deftheorem Def3 defines |. CLOSURE2:def 3 :
for b1 being functional set
for b2 being Function holds
( ( b1 <> {} implies ( b2 = |.b1.| iff ex b3 being non empty functional set st
( b3 = b1 & dom b2 = meet { (dom b4) where B is Element of b3 : verum } & ( for b4 being set st b4 in dom b2 holds
b2 . b4 = { (b5 . b4) where B is Element of b3 : verum } ) ) ) ) & ( not b1 <> {} implies ( b2 = |.b1.| iff b2 = {} ) ) );

theorem Th14: :: CLOSURE2:14
for b1 being set
for b2 being ManySortedSet of b1
for b3 being non empty SubsetFamily of b2 holds dom |.b3.| = b1
proof end;

registration
let c1 be empty functional set ;
cluster |.a1.| -> empty functional ;
coherence
|.c1.| is empty by Def3;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be SubsetFamily of c2;
func |:c3:| -> ManySortedSet of a1 equals :Def4: :: CLOSURE2:def 4
|.a3.| if a3 <> {}
otherwise [0] a1;
coherence
( ( c3 <> {} implies |.c3.| is ManySortedSet of c1 ) & ( not c3 <> {} implies [0] c1 is ManySortedSet of c1 ) )
proof end;
consistency
for b1 being ManySortedSet of c1 holds verum ;
end;

:: deftheorem Def4 defines |: CLOSURE2:def 4 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2 holds
( ( b3 <> {} implies |:b3:| = |.b3.| ) & ( not b3 <> {} implies |:b3:| = [0] b1 ) );

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be empty SubsetFamily of c2;
cluster |:a3:| -> V4 ;
coherence
|:c3:| is empty-yielding
proof end;
end;

theorem Th15: :: CLOSURE2:15
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2 st not b3 is empty holds
for b4 being set st b4 in b1 holds
|:b3:| . b4 = { (b5 . b4) where B is Element of Bool b2 : b5 in b3 }
proof end;

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be non empty SubsetFamily of c2;
cluster |:a3:| -> V3 ;
coherence
|:c3:| is non-empty
proof end;
end;

theorem Th16: :: CLOSURE2:16
for b1 being Function holds dom |.{b1}.| = dom b1
proof end;

theorem Th17: :: CLOSURE2:17
for b1, b2 being Function holds dom |.{b1,b2}.| = (dom b1) /\ (dom b2)
proof end;

theorem Th18: :: CLOSURE2:18
for b1 being set
for b2 being Function st b1 in dom b2 holds
|.{b2}.| . b1 = {(b2 . b1)}
proof end;

theorem Th19: :: CLOSURE2:19
for b1, b2 being set
for b3 being ManySortedSet of b2
for b4 being Function
for b5 being SubsetFamily of b3 st b1 in b2 & b5 = {b4} holds
|:b5:| . b1 = {(b4 . b1)}
proof end;

theorem Th20: :: CLOSURE2:20
for b1 being set
for b2, b3 being Function st b1 in dom |.{b2,b3}.| holds
|.{b2,b3}.| . b1 = {(b2 . b1),(b3 . b1)}
proof end;

theorem Th21: :: CLOSURE2:21
for b1, b2 being set
for b3 being ManySortedSet of b2
for b4, b5 being Function
for b6 being SubsetFamily of b3 st b1 in b2 & b6 = {b4,b5} holds
|:b6:| . b1 = {(b4 . b1),(b5 . b1)}
proof end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be SubsetFamily of c2;
redefine func |: as |:c3:| -> MSSubsetFamily of a2;
coherence
|:c3:| is MSSubsetFamily of c2
proof end;
end;

theorem Th22: :: CLOSURE2:22
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being SubsetFamily of b2 st b3 in b4 holds
b3 in' |:b4:|
proof end;

theorem Th23: :: CLOSURE2:23
for b1 being set
for b2, b3, b4 being ManySortedSet of b1
for b5 being SubsetFamily of b2 st b5 = {b3,b4} holds
union |:b5:| = b3 \/ b4
proof end;

theorem Th24: :: CLOSURE2:24
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2
for b4, b5 being Element of Bool b2 st b3 = {b4,b5} holds
meet |:b3:| = b4 /\ b5
proof end;

theorem Th25: :: CLOSURE2:25
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2
for b4 being ManySortedSubset of b2 st ( for b5 being ManySortedSet of b1 st b5 in b3 holds
b4 c=' b5 ) holds
b4 c=' meet |:b3:|
proof end;

theorem Th26: :: CLOSURE2:26
for b1 being set
for b2 being ManySortedSet of b1 holds |:(Bool b2):| = bool b2
proof end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be SubsetFamily of c2;
attr a3 is additive means :: CLOSURE2:def 5
for b1, b2 being ManySortedSet of a1 st b1 in a3 & b2 in a3 holds
b1 \/ b2 in a3;
attr a3 is absolutely-additive means :Def6: :: CLOSURE2:def 6
for b1 being SubsetFamily of a2 st b1 c= a3 holds
union |:b1:| in a3;
attr a3 is multiplicative means :: CLOSURE2:def 7
for b1, b2 being ManySortedSet of a1 st b1 in a3 & b2 in a3 holds
b1 /\ b2 in a3;
attr a3 is absolutely-multiplicative means :Def8: :: CLOSURE2:def 8
for b1 being SubsetFamily of a2 st b1 c= a3 holds
meet |:b1:| in a3;
attr a3 is properly-upper-bound means :Def9: :: CLOSURE2:def 9
a2 in a3;
attr a3 is properly-lower-bound means :Def10: :: CLOSURE2:def 10
 [0] a1 in a3;
end;

:: deftheorem Def5 defines additive CLOSURE2:def 5 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2 holds
( b3 is additive iff for b4, b5 being ManySortedSet of b1 st b4 in b3 & b5 in b3 holds
b4 \/ b5 in b3 );

:: deftheorem Def6 defines absolutely-additive CLOSURE2:def 6 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2 holds
( b3 is absolutely-additive iff for b4 being SubsetFamily of b2 st b4 c= b3 holds
union |:b4:| in b3 );

:: deftheorem Def7 defines multiplicative CLOSURE2:def 7 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2 holds
( b3 is multiplicative iff for b4, b5 being ManySortedSet of b1 st b4 in b3 & b5 in b3 holds
b4 /\ b5 in b3 );

:: deftheorem Def8 defines absolutely-multiplicative CLOSURE2:def 8 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2 holds
( b3 is absolutely-multiplicative iff for b4 being SubsetFamily of b2 st b4 c= b3 holds
meet |:b4:| in b3 );

:: deftheorem Def9 defines properly-upper-bound CLOSURE2:def 9 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2 holds
( b3 is properly-upper-bound iff b2 in b3 );

:: deftheorem Def10 defines properly-lower-bound CLOSURE2:def 10 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SubsetFamily of b2 holds
( b3 is properly-lower-bound iff [0] b1 in b3 );

Lemma24: for b1 being set
for b2 being ManySortedSet of b1 holds
( Bool b2 is additive & Bool b2 is absolutely-additive & Bool b2 is multiplicative & Bool b2 is absolutely-multiplicative & Bool b2 is properly-upper-bound & Bool b2 is properly-lower-bound )
proof end;

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool a2);
existence
ex b1 being SubsetFamily of c2 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 end;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
redefine func Bool as Bool c2 -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of a2;
coherence
Bool c2 is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of c2 by Lemma24;
end;

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster absolutely-additive -> additive Element of bool (Bool a2);
coherence
for b1 being SubsetFamily of c2 st b1 is absolutely-additive holds
b1 is additive
proof end;
end;

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster absolutely-multiplicative -> multiplicative Element of bool (Bool a2);
coherence
for b1 being SubsetFamily of c2 st b1 is absolutely-multiplicative holds
b1 is multiplicative
proof end;
end;

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

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

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

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

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
mode SetOp of a2 is Function of Bool a2, Bool a2;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be SetOp of c2;
let c4 be Element of Bool c2;
redefine func . as c3 . c4 -> Element of Bool a2;
coherence
c3 . c4 is Element of Bool c2
proof end;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be SetOp of c2;
canceled;
attr a3 is reflexive means :Def12: :: CLOSURE2:def 12
for b1 being Element of Bool a2 holds b1 c=' a3 . b1;
attr a3 is monotonic means :Def13: :: CLOSURE2:def 13
for b1, b2 being Element of Bool a2 st b1 c=' b2 holds
a3 . b1 c=' a3 . b2;
attr a3 is idempotent means :Def14: :: CLOSURE2:def 14
for b1 being Element of Bool a2 holds a3 . b1 = a3 . (a3 . b1);
attr a3 is topological means :Def15: :: CLOSURE2:def 15
for b1, b2 being Element of Bool a2 holds a3 . (b1 \/ b2) = (a3 . b1) \/ (a3 . b2);
end;

:: deftheorem Def11 CLOSURE2:def 11 :
canceled;

:: deftheorem Def12 defines reflexive CLOSURE2:def 12 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SetOp of b2 holds
( b3 is reflexive iff for b4 being Element of Bool b2 holds b4 c=' b3 . b4 );

:: deftheorem Def13 defines monotonic CLOSURE2:def 13 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SetOp of b2 holds
( b3 is monotonic iff for b4, b5 being Element of Bool b2 st b4 c=' b5 holds
b3 . b4 c=' b3 . b5 );

:: deftheorem Def14 defines idempotent CLOSURE2:def 14 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SetOp of b2 holds
( b3 is idempotent iff for b4 being Element of Bool b2 holds b3 . b4 = b3 . (b3 . b4) );

:: deftheorem Def15 defines topological CLOSURE2:def 15 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SetOp of b2 holds
( b3 is topological iff for b4, b5 being Element of Bool b2 holds b3 . (b4 \/ b5) = (b3 . b4) \/ (b3 . b5) );

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster reflexive monotonic idempotent topological M4( Bool a2, Bool a2);
existence
ex b1 being SetOp of c2 st
( b1 is reflexive & b1 is monotonic & b1 is idempotent & b1 is topological )
proof end;
end;

theorem Th27: :: CLOSURE2:27
for b1 being set
for b2 being ManySortedSet of b1 holds id (Bool b2) is reflexive SetOp of b2
proof end;

theorem Th28: :: CLOSURE2:28
for b1 being set
for b2 being ManySortedSet of b1 holds id (Bool b2) is monotonic SetOp of b2
proof end;

theorem Th29: :: CLOSURE2:29
for b1 being set
for b2 being ManySortedSet of b1 holds id (Bool b2) is idempotent SetOp of b2
proof end;

theorem Th30: :: CLOSURE2:30
for b1 being set
for b2 being ManySortedSet of b1 holds id (Bool b2) is topological SetOp of b2
proof end;

theorem Th31: :: CLOSURE2:31
for b1 being set
for b2 being ManySortedSet of b1
for b3 being Element of Bool b2
for b4 being SetOp of b2 st b3 = b2 & b4 is reflexive holds
b3 = b4 . b3
proof end;

theorem Th32: :: CLOSURE2:32
for b1 being set
for b2 being ManySortedSet of b1
for b3 being SetOp of b2 st b3 is reflexive & ( for b4 being Element of Bool b2 holds b3 . b4 c= b4 ) holds
b3 is idempotent
proof end;

theorem Th33: :: CLOSURE2:33
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being Element of Bool b2
for b5 being SetOp of b2
for b6 being Element of Bool b2 st b6 = b3 /\ b4 & b5 is monotonic holds
b5 . b6 c= (b5 . b3) /\ (b5 . b4)
proof end;

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster topological -> monotonic M4( Bool a2, Bool a2);
coherence
for b1 being SetOp of c2 st b1 is topological holds
b1 is monotonic
proof end;
end;

theorem Th34: :: CLOSURE2:34
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being Element of Bool b2
for b5 being SetOp of b2
for b6 being Element of Bool b2 st b6 = b3 \ b4 & b5 is topological holds
(b5 . b3) \ (b5 . b4) c= b5 . b6
proof end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3, c4 be SetOp of c2;
redefine func * as c4 * c3 -> SetOp of a2;
coherence
c3 * c4 is SetOp of c2
proof end;
end;

theorem Th35: :: CLOSURE2:35
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being SetOp of b2 st b3 is reflexive & b4 is reflexive holds
b3 * b4 is reflexive
proof end;

theorem Th36: :: CLOSURE2:36
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being SetOp of b2 st b3 is monotonic & b4 is monotonic holds
b3 * b4 is monotonic
proof end;

theorem Th37: :: CLOSURE2:37
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being SetOp of b2 st b3 is idempotent & b4 is idempotent & b3 * b4 = b4 * b3 holds
b3 * b4 is idempotent
proof end;

theorem Th38: :: CLOSURE2:38
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being SetOp of b2 st b3 is topological & b4 is topological holds
b3 * b4 is topological
proof end;

definition
let c1 be 1-sorted ;
attr a2 is strict;
struct ClosureStr of c1 -> many-sorted of a1;
aggr ClosureStr(# Sorts, Family #) -> ClosureStr of a1;
sel Family c2 -> SubsetFamily of the Sorts of a2;
end;

definition
let c1 be 1-sorted ;
let c2 be ClosureStr of c1;
attr a2 is additive means :Def16: :: CLOSURE2:def 16
the Family of a2 is additive;
attr a2 is absolutely-additive means :Def17: :: CLOSURE2:def 17
the Family of a2 is absolutely-additive;
attr a2 is multiplicative means :Def18: :: CLOSURE2:def 18
the Family of a2 is multiplicative;
attr a2 is absolutely-multiplicative means :Def19: :: CLOSURE2:def 19
the Family of a2 is absolutely-multiplicative;
attr a2 is properly-upper-bound means :Def20: :: CLOSURE2:def 20
the Family of a2 is properly-upper-bound;
attr a2 is properly-lower-bound means :Def21: :: CLOSURE2:def 21
the Family of a2 is properly-lower-bound;
end;

:: deftheorem Def16 defines additive CLOSURE2:def 16 :
for b1 being 1-sorted
for b2 being ClosureStr of b1 holds
( b2 is additive iff the Family of b2 is additive );

:: deftheorem Def17 defines absolutely-additive CLOSURE2:def 17 :
for b1 being 1-sorted
for b2 being ClosureStr of b1 holds
( b2 is absolutely-additive iff the Family of b2 is absolutely-additive );

:: deftheorem Def18 defines multiplicative CLOSURE2:def 18 :
for b1 being 1-sorted
for b2 being ClosureStr of b1 holds
( b2 is multiplicative iff the Family of b2 is multiplicative );

:: deftheorem Def19 defines absolutely-multiplicative CLOSURE2:def 19 :
for b1 being 1-sorted
for b2 being ClosureStr of b1 holds
( b2 is absolutely-multiplicative iff the Family of b2 is absolutely-multiplicative );

:: deftheorem Def20 defines properly-upper-bound CLOSURE2:def 20 :
for b1 being 1-sorted
for b2 being ClosureStr of b1 holds
( b2 is properly-upper-bound iff the Family of b2 is properly-upper-bound );

:: deftheorem Def21 defines properly-lower-bound CLOSURE2:def 21 :
for b1 being 1-sorted
for b2 being ClosureStr of b1 holds
( b2 is properly-lower-bound iff the Family of b2 is properly-lower-bound );

definition
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
func Full c2 -> ClosureStr of a1 equals :: CLOSURE2:def 22
 ClosureStr(# the Sorts of a2,(Bool the Sorts of a2) #);
correctness
coherence
ClosureStr(# the Sorts of c2,(Bool the Sorts of c2) #) is ClosureStr of c1;
;
end;

:: deftheorem Def22 defines Full CLOSURE2:def 22 :
for b1 being 1-sorted
for b2 being many-sorted of b1 holds Full b2 = ClosureStr(# the Sorts of b2,(Bool the Sorts of b2) #);

registration
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
cluster Full a2 -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence
( Full c2 is strict & Full c2 is additive & Full c2 is absolutely-additive & Full c2 is multiplicative & Full c2 is absolutely-multiplicative & Full c2 is properly-upper-bound & Full c2 is properly-lower-bound )
proof end;
end;

registration
let c1 be 1-sorted ;
let c2 be non-empty many-sorted of c1;
cluster Full a2 -> non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence
Full c2 is non-empty by MSUALG_1:def 8;
end;

registration
let c1 be 1-sorted ;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ClosureStr of a1;
existence
ex b1 being ClosureStr of c1 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 end;
end;

registration
let c1 be 1-sorted ;
let c2 be additive ClosureStr of c1;
cluster the Family of a2 -> additive ;
coherence
the Family of c2 is additive by Def16;
end;

registration
let c1 be 1-sorted ;
let c2 be absolutely-additive ClosureStr of c1;
cluster the Family of a2 -> non empty additive absolutely-additive properly-lower-bound ;
coherence
the Family of c2 is absolutely-additive by Def17;
end;

registration
let c1 be 1-sorted ;
let c2 be multiplicative ClosureStr of c1;
cluster the Family of a2 -> multiplicative ;
coherence
the Family of c2 is multiplicative by Def18;
end;

registration
let c1 be 1-sorted ;
let c2 be absolutely-multiplicative ClosureStr of c1;
cluster the Family of a2 -> non empty multiplicative absolutely-multiplicative properly-upper-bound ;
coherence
the Family of c2 is absolutely-multiplicative by Def19;
end;

registration
let c1 be 1-sorted ;
let c2 be properly-upper-bound ClosureStr of c1;
cluster the Family of a2 -> non empty properly-upper-bound ;
coherence
the Family of c2 is properly-upper-bound by Def20;
end;

registration
let c1 be 1-sorted ;
let c2 be properly-lower-bound ClosureStr of c1;
cluster the Family of a2 -> non empty properly-lower-bound ;
coherence
the Family of c2 is properly-lower-bound by Def21;
end;

registration
let c1 be 1-sorted ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be SubsetFamily of c2;
cluster ClosureStr(# a2,a3 #) -> non-empty ;
coherence
ClosureStr(# c2,c3 #) is non-empty
proof end;
end;

registration
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
let c3 be additive SubsetFamily of the Sorts of c2;
cluster ClosureStr(# the Sorts of a2,a3 #) -> additive ;
coherence
ClosureStr(# the Sorts of c2,c3 #) is additive by Def16;
end;

registration
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
let c3 be absolutely-additive SubsetFamily of the Sorts of c2;
cluster ClosureStr(# the Sorts of a2,a3 #) -> additive absolutely-additive ;
coherence
ClosureStr(# the Sorts of c2,c3 #) is absolutely-additive by Def17;
end;

registration
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
let c3 be multiplicative SubsetFamily of the Sorts of c2;
cluster ClosureStr(# the Sorts of a2,a3 #) -> multiplicative ;
coherence
ClosureStr(# the Sorts of c2,c3 #) is multiplicative by Def18;
end;

registration
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
let c3 be absolutely-multiplicative SubsetFamily of the Sorts of c2;
cluster ClosureStr(# the Sorts of a2,a3 #) -> multiplicative absolutely-multiplicative ;
coherence
ClosureStr(# the Sorts of c2,c3 #) is absolutely-multiplicative by Def19;
end;

registration
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
let c3 be properly-upper-bound SubsetFamily of the Sorts of c2;
cluster ClosureStr(# the Sorts of a2,a3 #) -> properly-upper-bound ;
coherence
ClosureStr(# the Sorts of c2,c3 #) is properly-upper-bound by Def20;
end;

registration
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
let c3 be properly-lower-bound SubsetFamily of the Sorts of c2;
cluster ClosureStr(# the Sorts of a2,a3 #) -> properly-lower-bound ;
coherence
ClosureStr(# the Sorts of c2,c3 #) is properly-lower-bound by Def21;
end;

registration
let c1 be 1-sorted ;
cluster absolutely-additive -> additive ClosureStr of a1;
coherence
for b1 being ClosureStr of c1 st b1 is absolutely-additive holds
b1 is additive
proof end;
end;

registration
let c1 be 1-sorted ;
cluster absolutely-multiplicative -> multiplicative ClosureStr of a1;
coherence
for b1 being ClosureStr of c1 st b1 is absolutely-multiplicative holds
b1 is multiplicative
proof end;
end;

registration
let c1 be 1-sorted ;
cluster absolutely-multiplicative -> properly-upper-bound ClosureStr of a1;
coherence
for b1 being ClosureStr of c1 st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proof end;
end;

registration
let c1 be 1-sorted ;
cluster absolutely-additive -> properly-lower-bound ClosureStr of a1;
coherence
for b1 being ClosureStr of c1 st b1 is absolutely-additive holds
b1 is properly-lower-bound
proof end;
end;

definition
let c1 be 1-sorted ;
mode ClosureSystem of a1 is absolutely-multiplicative ClosureStr of a1;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
mode ClosureOperator of a2 is reflexive monotonic idempotent SetOp of a2;
end;

theorem Th39: :: CLOSURE2:39
for b1 being 1-sorted
for b2 being ManySortedSet of the carrier of b1
for b3 being reflexive monotonic SetOp of b2
for b4 being SubsetFamily of b2 st b4 = { b5 where B is Element of Bool b2 : b3 . b5 = b5 } holds
ClosureStr(# b2,b4 #) is ClosureSystem of b1
proof end;

definition
let c1 be 1-sorted ;
let c2 be ManySortedSet of the carrier of c1;
let c3 be ClosureOperator of c2;
func ClOp->ClSys c3 -> strict ClosureSystem of a1 means :Def23: :: CLOSURE2:def 23
( the Sorts of a4 = a2 & the Family of a4 = { b1 where B is Element of Bool a2 : a3 . b1 = b1 } );
existence
ex b1 being strict ClosureSystem of c1 st
( the Sorts of b1 = c2 & the Family of b1 = { b2 where B is Element of Bool c2 : c3 . b2 = b2 } )
proof end;
uniqueness
for b1, b2 being strict ClosureSystem of c1 st the Sorts of b1 = c2 & the Family of b1 = { b3 where B is Element of Bool c2 : c3 . b3 = b3 } & the Sorts of b2 = c2 & the Family of b2 = { b3 where B is Element of Bool c2 : c3 . b3 = b3 } holds
b1 = b2 ;
end;

:: deftheorem Def23 defines ClOp->ClSys CLOSURE2:def 23 :
for b1 being 1-sorted
for b2 being ManySortedSet of the carrier of b1
for b3 being ClosureOperator of b2
for b4 being strict ClosureSystem of b1 holds
( b4 = ClOp->ClSys b3 iff ( the Sorts of b4 = b2 & the Family of b4 = { b5 where B is Element of Bool b2 : b3 . b5 = b5 } ) );

definition
let c1 be 1-sorted ;
let c2 be ClosureSystem of c1;
let c3 be ManySortedSubset of the Sorts of c2;
func Cl c3 -> Element of Bool the Sorts of a2 means :Def24: :: CLOSURE2:def 24
ex b1 being SubsetFamily of the Sorts of a2 st
( a4 = meet |:b1:| & b1 = { b2 where B is Element of Bool the Sorts of a2 : ( a3 c=' b2 & b2 in the Family of a2 ) } );
existence
ex b1 being Element of Bool the Sorts of c2ex b2 being SubsetFamily of the Sorts of c2 st
( b1 = meet |:b2:| & b2 = { b3 where B is Element of Bool the Sorts of c2 : ( c3 c=' b3 & b3 in the Family of c2 ) } )
proof end;
uniqueness
for b1, b2 being Element of Bool the Sorts of c2 st ex b3 being SubsetFamily of the Sorts of c2 st
( b1 = meet |:b3:| & b3 = { b4 where B is Element of Bool the Sorts of c2 : ( c3 c=' b4 & b4 in the Family of c2 ) } ) & ex b3 being SubsetFamily of the Sorts of c2 st
( b2 = meet |:b3:| & b3 = { b4 where B is Element of Bool the Sorts of c2 : ( c3 c=' b4 & b4 in the Family of c2 ) } ) holds
b1 = b2 ;
end;

:: deftheorem Def24 defines Cl CLOSURE2:def 24 :
for b1 being 1-sorted
for b2 being ClosureSystem of b1
for b3 being ManySortedSubset of the Sorts of b2
for b4 being Element of Bool the Sorts of b2 holds
( b4 = Cl b3 iff ex b5 being SubsetFamily of the Sorts of b2 st
( b4 = meet |:b5:| & b5 = { b6 where B is Element of Bool the Sorts of b2 : ( b3 c=' b6 & b6 in the Family of b2 ) } ) );

theorem Th40: :: CLOSURE2:40
for b1 being 1-sorted
for b2 being ClosureSystem of b1
for b3 being Element of Bool the Sorts of b2
for b4 being SetOp of the Sorts of b2 st b3 in the Family of b2 & ( for b5 being Element of Bool the Sorts of b2 holds b4 . b5 = Cl b5 ) holds
b4 . b3 = b3
proof end;

theorem Th41: :: CLOSURE2:41
for b1 being 1-sorted
for b2 being ClosureSystem of b1
for b3 being Element of Bool the Sorts of b2
for b4 being SetOp of the Sorts of b2 st b4 . b3 = b3 & ( for b5 being Element of Bool the Sorts of b2 holds b4 . b5 = Cl b5 ) holds
b3 in the Family of b2
proof end;

theorem Th42: :: CLOSURE2:42
for b1 being 1-sorted
for b2 being ClosureSystem of b1
for b3 being SetOp of the Sorts of b2 st ( for b4 being Element of Bool the Sorts of b2 holds b3 . b4 = Cl b4 ) holds
( b3 is reflexive & b3 is monotonic & b3 is idempotent )
proof end;

definition
let c1 be 1-sorted ;
let c2 be ClosureSystem of c1;
func ClSys->ClOp c2 -> ClosureOperator of the Sorts of a2 means :Def25: :: CLOSURE2:def 25
for b1 being Element of Bool the Sorts of a2 holds a3 . b1 = Cl b1;
existence
ex b1 being ClosureOperator of the Sorts of c2 st
for b2 being Element of Bool the Sorts of c2 holds b1 . b2 = Cl b2
proof end;
uniqueness
for b1, b2 being ClosureOperator of the Sorts of c2 st ( for b3 being Element of Bool the Sorts of c2 holds b1 . b3 = Cl b3 ) & ( for b3 being Element of Bool the Sorts of c2 holds b2 . b3 = Cl b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines ClSys->ClOp CLOSURE2:def 25 :
for b1 being 1-sorted
for b2 being ClosureSystem of b1
for b3 being ClosureOperator of the Sorts of b2 holds
( b3 = ClSys->ClOp b2 iff for b4 being Element of Bool the Sorts of b2 holds b3 . b4 = Cl b4 );

theorem Th43: :: CLOSURE2:43
for b1 being 1-sorted
for b2 being ManySortedSet of the carrier of b1
for b3 being ClosureOperator of b2 holds ClSys->ClOp (ClOp->ClSys b3) = b3
proof end;

deffunc H1( set ) -> set = a1;

theorem Th44: :: CLOSURE2:44
for b1 being 1-sorted
for b2 being ClosureSystem of b1 holds ClOp->ClSys (ClSys->ClOp b2) = ClosureStr(# the Sorts of b2,the Family of b2 #)
proof end;