let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in {[a,b],[c,d],[e,f]} or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in {[a,b],[c,d],[e,f]} ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then ( x = [a,b] or x = [c,d] or x = [e,f] ) by ENUMSET1:def 1;
hence ex b₁, b₂ being object st x = [b₁,b₂] ; :: thesis: verum