let a be object ; :: according to RELAT_1:def 1 :: thesis: ( not a in {x,y} or ex b_{1}, b_{2} being object st a = [b_{1},b_{2}] )

assume a in {x,y} ; :: thesis: ex b_{1}, b_{2} being object st a = [b_{1},b_{2}]

then ( a = x or a = y ) by TARSKI:def 2;

then ex y, z being object st a = [y,z] by XTUPLE_0:def 1;

hence ex b_{1}, b_{2} being object st a = [b_{1},b_{2}]
; :: thesis: verum

assume a in {x,y} ; :: thesis: ex b

then ( a = x or a = y ) by TARSKI:def 2;

then ex y, z being object st a = [y,z] by XTUPLE_0:def 1;

hence ex b