theorem :: UNIALG_2:18

for U0 being strict Universal_Algebra holds GenUnivAlg ([#] the carrier of U0) = U0