let x, z be object ; :: thesis: for X being set holds
( z in X \ {x} iff ( z in X & z <> x ) )
let X be set ; :: thesis: ( z in X \ {x} iff ( z in X & z <> x ) )
( z in X \ {x} iff ( z in X & not z in {x} ) ) by XBOOLE_0:def 5;
hence ( z in X \ {x} iff ( z in X & z <> x ) ) by TARSKI:def 1; :: thesis: verum