let x be object ; :: thesis: for X being set st X /\ {x} = {x} holds
x in X
let X be set ; :: thesis: ( X /\ {x} = {x} implies x in X )
assume X /\ {x} = {x} ; :: thesis: x in X
then x in X /\ {x} by TARSKI:def 1;
hence x in X by XBOOLE_0:def 4; :: thesis: verum