( rng R c= Y & dom (R ~) = rng R ) by RELAT_1:20;
hence for b₁ being Relation st b₁ = R ~ holds
b₁ is Y -defined by RELAT_1:def 18; :: thesis: verum