:: deftheorem Def11 defines DeTrivial FOMODEL3:def 11 :
for X being non empty set
for x being Element of SmallestPartition X
for b₃ being Element of X holds
( b₃ = DeTrivial x iff x = {b₃} );