let x, 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 set ; :: 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 by XBOOLE_1:2; :: thesis: verum