let F, G be set ; :: thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)

per cases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;

suppose A1: ( F <> {} & G <> {} ) ; :: thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (UNION (F,G)) or x in (meet F) \/ (meet G) )
assume A2: x in meet (UNION (F,G)) ; :: thesis: x in (meet F) \/ (meet G)
assume A3: not x in (meet F) \/ (meet G) ; :: thesis: contradiction
then not x in meet F by XBOOLE_0:def 3;
then consider Y being set such that
A4: ( Y in F & not x in Y ) by A1, SETFAM_1:def 1;
not x in meet G by A3, XBOOLE_0:def 3;
then consider Z being set such that
A5: ( Z in G & not x in Z ) by A1, SETFAM_1:def 1;
( not x in Y \/ Z & Y \/ Z in UNION (F,G) ) by A4, A5, SETFAM_1:def 4, XBOOLE_0:def 3;
hence contradiction by A2, SETFAM_1:def 1; :: thesis: verum

end;

suppose ( F = {} or G = {} ) ; :: thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)

then UNION (F,G) = {} by Th29;
then meet (UNION (F,G)) = {} by SETFAM_1:def 1;
hence meet (UNION (F,G)) c= (meet F) \/ (meet G) ; :: thesis: verum

end;

end;