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