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