let A be Subset of R; :: thesis: A is Relation-like
let x be set ; :: according to RELAT_1:def 1 :: thesis: ( x in A implies ex y, z being set st x = [y,z] )
thus ( x in A implies ex y, z being set st x = [y,z] ) by Def1; :: thesis: verum