let a be object ; :: according to RELAT_1:def 1 :: thesis: ( not a in {x} or ex b₁, b₂ being object st a = [b₁,b₂] )
assume a in {x} ; :: thesis: ex b₁, b₂ being object st a = [b₁,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₁, b₂ being object st a = [b₁,b₂] ; :: thesis: verum