let I be set ; :: thesis: for M being ManySortedSet of 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 ; :: 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 ; :: according to MSSUBFAM:def 3 :: thesis: for B being ManySortedSet of st A in bool M & B in bool M holds
A \/ B in bool M
let B be ManySortedSet of ; :: 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:18;
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 4 :: 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:19; :: 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 ; :: according to MSSUBFAM:def 5 :: thesis: for B being ManySortedSet of st A in bool M & B in bool M holds
A /\ B in bool M
let B be ManySortedSet of ; :: 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 MBOOLEAN:15;
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 6 :: 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 23;
hence meet F in bool M by MBOOLEAN:19; :: thesis: verum

end;

thus bool M is properly-upper-bound :: thesis: bool M is properly-lower-bound

proof

thus M in bool M by MBOOLEAN:19; :: according to MSSUBFAM:def 7 :: thesis: verum

end;

thus bool M is properly-lower-bound :: thesis: verum

proof

[0] I c= M by MBOOLEAN:5;
hence [0] I in bool M by MBOOLEAN:1; :: according to MSSUBFAM:def 8 :: thesis: verum

end;