:: deftheorem defines SmallestPartition EQREL_1:def 5 :
for X being set holds SmallestPartition X = Class (id X);