theorem :: SETFAM_1:24

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