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;

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;

end;

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;hence x in (union F) \/ (union G) by XBOOLE_0:def 3; :: thesis: verum

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;hence x in (union F) \/ (union G) by XBOOLE_0:def 3; :: thesis: verum