let SF be SubsetFamily 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 ; :: according to CLOSURE2:def 7 :: 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 Def1;
then ( A c= M & B c= M ) by PBOOLE:def 23;
then reconsider ab = {A,B} as SubsetFamily of M by Th9;
( {A} c= SF & {B} c= SF ) by A2, ZFMISC_1:37;
then {A} \/ {B} c= SF by XBOOLE_1:8;
then {A,B} c= SF by ENUMSET1:41;
then meet |:ab:| in SF by A1, Def8;
hence A /\ B in SF by A2, Th24; :: thesis: verum