let X, Y be set ; :: thesis: for R being X -defined Y -valued Relation holds R c= [:X,Y:]
let R be X -defined Y -valued Relation; :: thesis: R c= [:X,Y:]
A1: R c= [:(dom R),(rng R):] by Th1;
( dom R c= X & rng R c= Y ) by Def16, Def17;
then [:(dom R),(rng R):] c= [:X,Y:] by ZFMISC_1:96;
hence R c= [:X,Y:] by A1; :: thesis: verum