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

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