theorem :: SUBSET_1:47

for X being non empty set
for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x}