let SF be SubsetFamily of M; :: thesis: ( SF is absolutely-additive implies SF is additive )
assume A1: SF is absolutely-additive ; :: thesis: SF is additive
let A be ManySortedSet of I; :: according to CLOSURE2:def 4 :: thesis: for B being ManySortedSet of I st A in SF & B in SF holds
A (\/) B in SF
let B be ManySortedSet of I; :: thesis: ( A in SF & B in SF implies A (\/) B in SF )
assume that
A2: A in SF and
A3: B in SF ; :: thesis: A (\/) B in SF
B is ManySortedSubset of M by A3, Def1;
then A4: B c= M by PBOOLE:def 18;
A is ManySortedSubset of M by A2, Def1;
then A c= M by PBOOLE:def 18;
then reconsider ab = {A,B} as SubsetFamily of M by A4, Th8;
( {A} c= SF & {B} c= SF ) by A2, A3, ZFMISC_1:31;
then {A} \/ {B} c= SF by XBOOLE_1:8;
then {A,B} c= SF by ENUMSET1:1;
then union |:ab:| in SF by A1;
hence A (\/) B in SF by Th22; :: thesis: verum