theorem :: MSSUBFAM:8
for I being set
for sf, sg, sh being Subset-Family of I st sh = sf \/ sg holds
Intersect sh = (Intersect sf) /\ (Intersect sg)