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

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

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 b_{1}, b_{2} being object st a = [b_{1},b_{2}]
; :: thesis: verum

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

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 b