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