let SF be MSSubsetFamily of M; :: thesis: ( SF is absolutely-multiplicative implies SF is multiplicative )
assume A1: SF is absolutely-multiplicative ; :: thesis: SF is multiplicative
let A be ManySortedSet of I; :: according to MSSUBFAM: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
A4: B is ManySortedSubset of M by A3, Th33;
then A5: B c= M by PBOOLE:def 18;
A6: A is ManySortedSubset of M by A2, Th33;
then A c= M by PBOOLE:def 18;
then reconsider ab = {A,B} as MSSubsetFamily of M by A5, Th39;
( {A} c= SF & {B} c= SF ) by A2, A3, PZFMISC1:33;
then {A} (\/) {B} c= SF by PBOOLE:16;
then {A,B} c= SF by PZFMISC1:10;
then meet ab in SF by A1;
hence A (/\) B in SF by A6, A4, Th51; :: thesis: verum