let A be non empty set ; :: thesis: not A misses A
ex x being set st x in A by XBOOLE_0:def 1;
hence not A misses A by XBOOLE_0:3; :: thesis: verum