theorem :: SETFAM_1:26

for X, SFY being set st SFY <> {} holds
X \ (union SFY) = meet (DIFFERENCE ({X},SFY))