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