let X, Y be set ; :: thesis: for r being X -defined Y -valued Relation holds r is Relation of X,Y
let r be X -defined Y -valued Relation; :: thesis: r is Relation of X,Y
( dom r c= X & rng r c= Y ) by RELAT_1:def 18, RELAT_1:def 19;
then ( [:(dom r),(rng r):] c= [:X,Y:] & r c= [:(dom r),(rng r):] ) by RELAT_1:7, ZFMISC_1:96;
hence r is Relation of X,Y by XBOOLE_1:1; :: thesis: verum