x in {x} by TARSKI:def 1;
hence ex z being object st z in {x} ; :: according to XBOOLE_0:def 1 :: thesis: verum