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 5 :: 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 Th11; :: 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 6 :: 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 23;
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 7 :: 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-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 8 :: 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 23;
then M in Bool M by Def1;
hence Bool M is properly-upper-bound by Def9; :: thesis: Bool M is properly-lower-bound
[[0]] I c= M by PBOOLE:49;
then [[0]] I is ManySortedSubset of M by PBOOLE:def 23;
hence [[0]] I in Bool M by Def1; :: according to CLOSURE2:def 10 :: thesis: verum