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} )

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 = {{}}

hence
( a is terminal implies ex x being set st a = {x} )
by Th33; :: thesis: verumA1:
{{}} in W
by CLASSES2:56, CLASSES2:57;

assume W = {{}} ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;assume W = {{}} ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum