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

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

end;

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;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