:: deftheorem defines UnSubAlLattice UNIALG_2:def 17 :
for U0 being with_const_op Universal_Algebra holds UnSubAlLattice U0 = LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);