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