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