let F, G be set ; :: thesis: ( F <> {} & G <> {} implies (union F) \/ (union G) = union (UNION F,G) )
assume A1: ( F <> {} & G <> {} ) ; :: thesis: (union F) \/ (union G) = union (UNION F,G)
thus (union F) \/ (union G) c= union (UNION F,G) :: according to XBOOLE_0:def 10 :: thesis: union (UNION F,G) c= (union F) \/ (union G)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (union F) \/ (union G) or x in union (UNION F,G) )
assume A2: x in (union F) \/ (union G) ; :: thesis: x in union (UNION F,G)

per cases ( x in union F or x in union G ) by A2, XBOOLE_0:def 3;

suppose x in union F ; :: thesis: x in union (UNION F,G)

then consider Y being set such that
A3: ( x in Y & Y in F ) by TARSKI:def 4;
consider W being set such that
A4: W in G by A1, XBOOLE_0:def 1;
set YW = Y \/ W;
A5: Y c= Y \/ W by XBOOLE_1:7;
Y \/ W in UNION F,G by A3, A4, SETFAM_1:def 4;
hence x in union (UNION F,G) by A3, A5, TARSKI:def 4; :: thesis: verum

end;

suppose x in union G ; :: thesis: x in union (UNION F,G)

then consider Y being set such that
A6: ( x in Y & Y in G ) by TARSKI:def 4;
consider W being set such that
A7: W in F by A1, XBOOLE_0:def 1;
set YW = W \/ Y;
A8: Y c= W \/ Y by XBOOLE_1:7;
W \/ Y in UNION F,G by A6, A7, SETFAM_1:def 4;
hence x in union (UNION F,G) by A6, A8, TARSKI:def 4; :: thesis: verum

end;

end;

end;

thus union (UNION F,G) c= (union F) \/ (union G) by Th27; :: thesis: verum