:: deftheorem defines is_multiplicative_with CARD_FIL:def 3 :
for X being non empty set
for N being Cardinal
for S being non empty Subset-Family of X holds
( S is_multiplicative_with N iff for S1 being non empty set st S1 c= S & card S1 in N holds
meet S1 in S );