theorem Th18: :: UNIALG_3:18

for U0 being strict with_const_op Universal_Algebra
for U1 being strict SubAlgebra of U0 holds (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0)