theorem :: UNIALG_3:19

for U0 being strict with_const_op Universal_Algebra holds Bottom (UnSubAlLattice U0) = GenUnivAlg (Constants U0)