rng (id P) = P by RELAT_1:71;
hence id P is IndexedPartition of X by Def3; :: thesis: verum