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