:: deftheorem Def12 defines peeler FOMODEL3:def 12 :
for X being non empty set
for b₂ being Function of (SmallestPartition X),X holds
( b₂ = peeler X iff for x being Element of SmallestPartition X holds b₂ . x = DeTrivial x );