theorem :: PARTIT1:38

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