for U0 being Universal_Algebra
for H being non empty Subset of U0
for o being operation of U0 st arity o = 0 holds
( H is_closed_on o iff o . {} in H )