let W be Universe; :: thesis: for f being Morphism of (Ens W) st f is epi holds
@ f is surjective
let f be Morphism of (Ens W); :: thesis: ( f is epi implies @ f is surjective )
( {} in W & {{}} in W ) by CLASSES2:56, CLASSES2:57;
then A1: {{},{{}}} in W by CLASSES2:58;
( {} in {{},{{}}} & {{}} in {{},{{}}} ) by TARSKI:def 2;
hence ( f is epi implies @ f is surjective ) by A1, Th37; :: thesis: verum