let a be set ; :: according to RELAT_1:def 1 :: thesis: ( not a in {x,y,z} or ex b₁, b₂ being set st a = [b₁,b₂] )
assume a in {x,y,z} ; :: thesis: ex b₁, b₂ being set st a = [b₁,b₂]
then ( a = x or a = y or a = z ) by ENUMSET1:def 1;
hence ex b₁, b₂ being set st a = [b₁,b₂] by Def1; :: thesis: verum