theorem :: ENS_1:35

for W being Universe
for a being Object of (Ens W) st a is terminal holds
ex x being set st a = {x}