let F, G be set ; :: thesis: ( not UNION (F,G) = {} or F = {} or G = {} )

assume A1: UNION (F,G) = {} ; :: thesis: ( F = {} or G = {} )

assume that

A2: F <> {} and

A3: G <> {} ; :: thesis: contradiction

consider X being object such that

A4: X in F by A2, XBOOLE_0:def 1;

consider Y being object such that

A5: Y in G by A3, XBOOLE_0:def 1;

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

X \/ Y in UNION (F,G) by A4, A5, SETFAM_1:def 4;

hence contradiction by A1; :: thesis: verum

assume A1: UNION (F,G) = {} ; :: thesis: ( F = {} or G = {} )

assume that

A2: F <> {} and

A3: G <> {} ; :: thesis: contradiction

consider X being object such that

A4: X in F by A2, XBOOLE_0:def 1;

consider Y being object such that

A5: Y in G by A3, XBOOLE_0:def 1;

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

X \/ Y in UNION (F,G) by A4, A5, SETFAM_1:def 4;

hence contradiction by A1; :: thesis: verum