rng (id R) = [#] R by RELAT_1:45;
hence (id R) /" is one-to-one by TOPS_2:50; :: thesis: verum