let z be set ; :: according to RELAT_1:def 1 :: thesis: ( z in [:a,b:] implies ex y, z being set st z = [y,z] )
assume z in [:a,b:] ; :: thesis: ex y, z being set st z = [y,z]
then ex x, y being set st
( x in a & y in b & [x,y] = z ) by ZFMISC_1:def 2;
hence ex y, z being set st z = [y,z] ; :: thesis: verum