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 ; :: according to MSSUBFAM:def 3 :: thesis: for B being ManySortedSet of st A in SF & B in SF holds
A \/ B in SF
let B be ManySortedSet of ; :: thesis: ( A in SF & B in SF implies A \/ B in SF )
assume A2: ( A in SF & B in SF ) ; :: thesis: A \/ B in SF
then ( A is ManySortedSubset of M & B is ManySortedSubset of M ) by Th33;
then ( A c= M & B c= M ) by PBOOLE:def 23;
then A3: {A,B} is MSSubsetFamily of M by Th39;
( {A} c= SF & {B} c= SF ) by A2, PZFMISC1:36;
then {A} \/ {B} c= SF by PBOOLE:18;
then {A,B} c= SF by PZFMISC1:11;
then union {A,B} in SF by A1, A3, Def4;
hence A \/ B in SF by PZFMISC1:35; :: thesis: verum