:: deftheorem defines Rel PARTIT1:def 7 :
for Y being non empty set
for b₂ being Function holds
( b₂ = Rel Y iff ( dom b₂ = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b₂ . x = ERl PA ) ) ) );