for F, G being set st F <> {} & G <> {} holds
meet (UNION (F,G)) = (meet F) \/ (meet G) by Th32, SETFAM_1:29;