theorem Th8: :: AUTALG_1:8

for UA being Universal_Algebra holds id the carrier of UA = 1_ (UAAutGroup UA)