theorem :: EQREL_1:37

for X being non empty set holds SmallestPartition X = { {x} where x is Element of X : verum }