let F, G be set ; :: thesis: ( F <> {} & G <> {} implies meet (UNION (F,G)) = (meet F) \/ (meet G) )
assume A1: ( F <> {} & G <> {} ) ; :: thesis: meet (UNION (F,G)) = (meet F) \/ (meet G)
thus meet (UNION (F,G)) c= (meet F) \/ (meet G) by Th32; :: according to XBOOLE_0:def 10 :: thesis: (meet F) \/ (meet G) c= meet (UNION (F,G))
thus (meet F) \/ (meet G) c= meet (UNION (F,G)) by A1, SETFAM_1:29; :: thesis: verum