r is Relation of X, bool Y by RELSET_1:def 1;
hence rng r is Subset-Family of Y by RELSET_1:12; :: thesis: verum