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 ;
not x in meet G by ;
then consider Z being set such that
A5: ( Z in G & not x in Z ) by ;
( not x in Y \/ Z & Y \/ Z in UNION (F,G) ) by ;
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;