theorem :: UNIALG_3:5

for U0 being Universal_Algebra holds Constants U0 = { (o . {}) where o is operation of U0 : arity o = 0 }