let F, G be set ; :: thesis: ( not INTERSECTION (F,G) = {} or F = {} or G = {} )
assume that
A1: INTERSECTION (F,G) = {} and
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 INTERSECTION (F,G) by A4, A5, SETFAM_1:def 5;
hence contradiction by A1; :: thesis: verum