let F, G be set ; :: thesis: union (UNION F,G) c= (union F) \/ (union G)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (UNION F,G) or x in (union F) \/ (union G) )
assume x in union (UNION F,G) ; :: thesis: x in (union F) \/ (union G)
then consider Y being set such that
A1: ( x in Y & Y in UNION F,G ) by TARSKI:def 4;
consider f, g being set such that
A2: ( f in F & g in G & Y = f \/ g ) by A1, SETFAM_1:def 4;

per cases ( x in f or x in g ) by A1, A2, XBOOLE_0:def 3;

suppose x in f ; :: thesis: x in (union F) \/ (union G)

then x in union F by A2, TARSKI:def 4;
hence x in (union F) \/ (union G) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in g ; :: thesis: x in (union F) \/ (union G)

then x in union G by A2, TARSKI:def 4;
hence x in (union F) \/ (union G) by XBOOLE_0:def 3; :: thesis: verum

end;

end;