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