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