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 MSSUBFAM:def 2 :: 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
then ( A c= M & B c= M ) by MBOOLEAN:1;
then A \/ B c= M by PBOOLE:16;
hence A \/ B in bool M by MBOOLEAN:1; :: 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 MSSubsetFamily of M; :: according to MSSUBFAM:def 3 :: 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 Th40;
hence union F in bool M by MBOOLEAN:18; :: 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 MSSUBFAM: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 that
A1: A in bool M and
B in bool M ; :: thesis: A /\ B in bool M
A c= M by A1, MBOOLEAN:1;
then A /\ B c= M by MBOOLEAN:14;
hence A /\ B in bool M by MBOOLEAN:1; :: 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 MSSubsetFamily of M; :: according to MSSUBFAM:def 5 :: thesis: ( F c= bool M implies meet F in bool M )
assume F c= bool M ; :: thesis: meet F in bool M
meet F c= M by PBOOLE:def 18;
hence meet F in bool M by MBOOLEAN:18; :: thesis: verum

end;

M in bool M by MBOOLEAN:18;
hence bool M is properly-upper-bound by Def7; :: thesis: bool M is properly-lower-bound
[[0]] I c= M by MBOOLEAN:5;
then [[0]] I in bool M by MBOOLEAN:1;
hence bool M is properly-lower-bound by Def8; :: thesis: verum