consider p being a_partition of X;
take id p ; :: thesis: ( rng (id p) is a_partition of X & id p is one-to-one )
thus ( rng (id p) is a_partition of X & id p is one-to-one ) by RELAT_1:71; :: thesis: verum