theorem Th20: :: PARTIT1:20

for Y being non empty set
for PA, PB being a_partition of Y holds
( PA '<' PB iff ERl PA c= ERl PB )