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