:: deftheorem defines MSSubAlLattice MSUALG_2:def 22 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);