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

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

then a = x by TARSKI: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} ; :: thesis: ex b

then a = x by TARSKI:def 1;

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

hence ex b