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