let X, Y be set ; :: thesis: ( X c= Y implies for R being X -defined Relation holds R is Y -defined )
assume A1: X c= Y ; :: thesis: for R being X -defined Relation holds R is Y -defined
let R be X -defined Relation; :: thesis: R is Y -defined
dom R c= X by Def16;
hence dom R c= Y by A1; :: according to RELAT_1:def 18 :: thesis: verum