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),(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