set XX = SmallestPartition X;
consider y being set such that
B1: ( x = {y} & y in X ) by RELSET_2:1;
reconsider yy = y as Element of X by B1;
take yy ; :: thesis: x = {yy}
thus x = {yy} by B1; :: thesis: verum