:: deftheorem Def3 defines PARTITIONS PARTIT1:def 3 :
for Y, b₂ being set holds
( b₂ = PARTITIONS Y iff for x being set holds
( x in b₂ iff x is a_partition of Y ) );