theorem :: MSSUBFAM:3

for I being set
for sf being Subset-Family of I st {} in sf holds
Intersect sf = {}