:: deftheorem defines Constants UNIALG_2:def 10 :
for U0 being Universal_Algebra holds Constants U0 = { a where a is Element of U0 : ex o being operation of U0 st
( arity o = 0 & a in rng o ) } ;