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