let a be object ; RELAT_1:def 1 ( not a in {x,y} or ex b1, b2 being object st a = [b1,b2] )
assume
a in {x,y}
; ex b1, b2 being object st a = [b1,b2]
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 b1, b2 being object st a = [b1,b2]
; verum