let F, G be set ; :: thesis: ( not UNION F,G = {} or F = {} or G = {} )
assume A1: UNION F,G = {} ; :: thesis: ( F = {} or G = {} )
assume A2: ( F <> {} & G <> {} ) ; :: thesis: contradiction
then consider X being set such that
A3: X in F by XBOOLE_0:def 1;
consider Y being set such that
A4: Y in G by A2, XBOOLE_0:def 1;
X \/ Y in UNION F,G by A3, A4, SETFAM_1:def 4;
hence contradiction by A1; :: thesis: verum