:: deftheorem Def11 defines with_const_op UNIALG_2:def 11 :
for IT being Universal_Algebra holds
( IT is with_const_op iff ex o being operation of IT st arity o = 0 );