let A, B be set ; :: thesis: for R being A -valued Relation holds R .: B c= A
let R be A -valued Relation; :: thesis: R .: B c= A
( R .: B c= rng R & rng R c= A ) by RELAT_1:111, RELAT_1:def 19;
hence R .: B c= A ; :: thesis: verum