for A being with_const_op Universal_Algebra holds UnSubAlLattice UAStr(# the carrier of A, the charact of A #), MSSubAlLattice (MSAlg UAStr(# the carrier of A, the charact of A #)) are_isomorphic