let F, G be set ; :: thesis: ( F <> {} & G <> {} implies (union F) \/ (union G) = union (UNION (F,G)) )

assume that

A1: F <> {} and

A2: 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)

assume that

A1: F <> {} and

A2: 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

thus
union (UNION (F,G)) c= (union F) \/ (union G)
by Th27; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union F) \/ (union G) or x in union (UNION (F,G)) )

assume A3: x in (union F) \/ (union G) ; :: thesis: x in union (UNION (F,G))

end;assume A3: 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 A3, XBOOLE_0:def 3;

end;

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

consider W being object such that

A5: W in G by A2, XBOOLE_0:def 1;

consider Y being set such that

A6: x in Y and

A7: Y in F by A4, TARSKI:def 4;

reconsider Y = Y, W = W as set by TARSKI:1;

set YW = Y \/ W;

( Y c= Y \/ W & Y \/ W in UNION (F,G) ) by A7, A5, SETFAM_1:def 4, XBOOLE_1:7;

hence x in union (UNION (F,G)) by A6, TARSKI:def 4; :: thesis: verum

end;A5: W in G by A2, XBOOLE_0:def 1;

consider Y being set such that

A6: x in Y and

A7: Y in F by A4, TARSKI:def 4;

reconsider Y = Y, W = W as set by TARSKI:1;

set YW = Y \/ W;

( Y c= Y \/ W & Y \/ W in UNION (F,G) ) by A7, A5, SETFAM_1:def 4, XBOOLE_1:7;

hence x in union (UNION (F,G)) by A6, TARSKI:def 4; :: thesis: verum

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

consider W being object such that

A9: W in F by A1, XBOOLE_0:def 1;

consider Y being set such that

A10: x in Y and

A11: Y in G by A8, TARSKI:def 4;

reconsider Y = Y, W = W as set by TARSKI:1;

set YW = W \/ Y;

( Y c= W \/ Y & W \/ Y in UNION (F,G) ) by A11, A9, SETFAM_1:def 4, XBOOLE_1:7;

hence x in union (UNION (F,G)) by A10, TARSKI:def 4; :: thesis: verum

end;A9: W in F by A1, XBOOLE_0:def 1;

consider Y being set such that

A10: x in Y and

A11: Y in G by A8, TARSKI:def 4;

reconsider Y = Y, W = W as set by TARSKI:1;

set YW = W \/ Y;

( Y c= W \/ Y & W \/ Y in UNION (F,G) ) by A11, A9, SETFAM_1:def 4, XBOOLE_1:7;

hence x in union (UNION (F,G)) by A10, TARSKI:def 4; :: thesis: verum