let UA be Universal_Algebra; :: thesis: id the carrier of UA in UAAut UA
id the carrier of UA is_isomorphism by Th1;
hence id the carrier of UA in UAAut UA by Def1; :: thesis: verum