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:62, CLASSES2:63;
then A1: {{} ,{{} }} in W by CLASSES2:64;
( {} in {{} ,{{} }} & {{} } in {{} ,{{} }} ) by TARSKI:def 2;
hence ( f is epi implies @ f is surjective ) by A1, Th37; :: thesis: verum