let F, G be set ; :: thesis: union (UNION (F,G)) c= (union F) \/ (union G)
let x be object ; :: 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 and
A2: Y in UNION (F,G) by TARSKI:def 4;
consider f, g being set such that
A3: f in F and
A4: g in G and
A5: Y = f \/ g by A2, SETFAM_1:def 4;
per cases ( x in f or x in g ) by A1, A5, XBOOLE_0:def 3;
suppose x in f ; :: thesis: x in (union F) \/ (union G)
then x in union F by A3, 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 A4, TARSKI:def 4;
hence x in (union F) \/ (union G) by XBOOLE_0:def 3; :: thesis: verum
end;
end;