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