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

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