let x, y be set ; :: thesis: {[x,y]} is Relation-like
thus for a being set st a in {[x,y]} holds
ex x, y being set st a = [x,y] :: according to RELAT_1:def 1 :: thesis: verum

proof

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

end;