let x be object ; :: thesis: for X being set st not x in X holds
{x} misses X
let X be set ; :: thesis: ( not x in X implies {x} misses X )
assume A1: not x in X ; :: thesis: {x} misses X
thus {x} /\ X c= {} :: according to XBOOLE_0:def 7,XBOOLE_0:def 10 :: thesis: {} c= {x} /\ X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {x} /\ X or y in {} )
assume y in {x} /\ X ; :: thesis: y in {}
then ( y in {x} & y in X ) by XBOOLE_0:def 4;
hence y in {} by A1, TARSKI:def 1; :: thesis: verum

end;

thus {} c= {x} /\ X ; :: thesis: verum