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:40; :: thesis: verum