let x, X be set ; :: thesis: ( {x} \ X = {} iff x in X )
( {x} \ X = {} iff {x} c= X ) by XBOOLE_1:37;
hence ( {x} \ X = {} iff x in X ) by Lm1; :: thesis: verum