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 by Th10; :: 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 )
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 5 :: 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 18;
hence union |:F:| in Bool M by Def1; :: thesis: verum
end;
thus Bool M is multiplicative by Th9; :: thesis: ( Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
thus Bool M is absolutely-multiplicative by Def1; :: thesis: ( Bool M is properly-upper-bound & Bool M is properly-lower-bound )
M is ManySortedSubset of M by PBOOLE:def 18;
then M in Bool M by Def1;
hence Bool M is properly-upper-bound ; :: thesis: Bool M is properly-lower-bound
EmptyMS I c= M by PBOOLE:43;
then EmptyMS I is ManySortedSubset of M by PBOOLE:def 18;
hence EmptyMS I in Bool M by Def1; :: according to CLOSURE2:def 9 :: thesis: verum