let X be set ; :: thesis: X misses {}
assume X meets {} ; :: thesis: contradiction
then ex x being set st
( x in X & x in {} ) by XBOOLE_0:3;
hence contradiction ; :: thesis: verum