let W be Universe; :: thesis: for a being Object of (Ens W) st a is terminal holds
ex x being set st a = {x}
let a be Object of (Ens W); :: thesis: ( a is terminal implies ex x being set st a = {x} )
now :: thesis: not W = {{}}
A1: {{}} in W by CLASSES2:56, CLASSES2:57;
assume W = {{}} ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum
end;
hence ( a is terminal implies ex x being set st a = {x} ) by Th33; :: thesis: verum