( rng (X | R) c= rng R & rng R c= A ) by Def19, Th118;
hence rng (X | R) c= A by XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: X | R is X -valued
thus rng (X | R) c= X by Th116; :: according to RELAT_1:def 19 :: thesis: verum