let x be object ; :: according to RELAT_1:def 1 :: thesis: ( x in {[a,b]} implies ex y, z being object st x = [y,z] )
assume x in {[a,b]} ; :: thesis: ex y, z being object st x = [y,z]
then x = [a,b] by TARSKI:def 1;
hence ex y, z being object st x = [y,z] ; :: thesis: verum