:: deftheorem Def3 defines Constants MSUALG_2:def 3 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for s being SortSymbol of S
for b₄ being Subset of ( the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} implies ( b₄ = Constants (U0,s) iff ex A being non empty set st
( A = the Sorts of U0 . s & b₄ = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) ) & ( not the Sorts of U0 . s <> {} implies ( b₄ = Constants (U0,s) iff b₄ = {} ) ) );