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