let SF be MSSubsetFamily 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 MSSUBFAM:def 2 :: 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
( {A} c= SF & {B} c= SF ) by A2, A3, PZFMISC1:33;
then {A} (\/) {B} c= SF by PBOOLE:16;
then A4: {A,B} c= SF by PZFMISC1:10;
B is ManySortedSubset of M by A3, Th33;
then A5: B c= M by PBOOLE:def 18;
A is ManySortedSubset of M by A2, Th33;
then A c= M by PBOOLE:def 18;
then {A,B} is MSSubsetFamily of M by A5, Th39;
then union {A,B} in SF by A1, A4;
hence A (\/) B in SF by PZFMISC1:32; :: thesis: verum