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 by Th40, MBOOLEAN:18; :: thesis: ( 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 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 by PBOOLE:def 18, MBOOLEAN:18; :: thesis: ( bool M is properly-upper-bound & bool M is properly-lower-bound )
M in bool M by MBOOLEAN:18;
hence bool M is properly-upper-bound ; :: thesis: bool M is properly-lower-bound
EmptyMS I c= M by MBOOLEAN:5;
then EmptyMS I in bool M by MBOOLEAN:1;
hence bool M is properly-lower-bound ; :: thesis: verum