consider P being a_partition of A;
take id P ; :: thesis: rng (id P) is a_partition of A
thus rng (id P) is a_partition of A by RELAT_1:71; :: thesis: verum