theorem :: PARTIT1:31

for Y being non empty set holds %I Y = { B where B is Subset of Y : ex x being set st
( B = {x} & x in Y ) }