for X being set
for P being a_partition of X holds P = Class (ERl P)