let UA be Universal_Algebra; :: thesis: id the carrier of UA is_isomorphism
set I = id the carrier of UA;
id the carrier of UA is_homomorphism by ALG_1:5;
hence id the carrier of UA is_monomorphism ; :: according to ALG_1:def 4 :: thesis: id the carrier of UA is_epimorphism
( id the carrier of UA is_homomorphism & rng (id the carrier of UA) = the carrier of UA ) by ALG_1:5, RELAT_1:45;
hence id the carrier of UA is_epimorphism ; :: thesis: verum