theorem :: SETFAM_1:27

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