let W be Universe; :: thesis: for a being Object of st a is terminal holds
ex x being set st a = {x}
let a be Object of ; :: thesis: ( a is terminal implies ex x being set st a = {x} )

now

A1: {{} } in W by CLASSES2:62, CLASSES2:63;
assume W = {{} } ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum

end;

hence ( a is terminal implies ex x being set st a = {x} ) by Th34; :: thesis: verum