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