let x, X be set ; :: thesis: ( {x} misses X implies not x in X )
assume that
A1: {x} /\ X = {} and
A2: x in X ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
x in {x} by TARSKI:def 1;
then x in {x} /\ X by A2, XBOOLE_0:def 4;
hence contradiction by A1; :: thesis: verum