let x be object ; :: thesis: for X being set st {x} misses X holds
not x in X
let X be set ; :: thesis: ( {x} misses X implies not x in X )
A1: x in {x} by TARSKI:def 1;
assume ( {x} /\ X = {} & x in X ) ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
hence contradiction by A1, XBOOLE_0:def 4; :: thesis: verum