:: deftheorem Def22 defines TrivialOSA OSALG_1:def 22 :
for S being OrderSortedSign
for z being non empty set
for z1 being Element of z
for b₄ being strict OSAlgebra of S holds
( b₄ = TrivialOSA (S,z,z1) iff ( the Sorts of b₄ = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b₄) = (Args (o,b₄)) --> z1 ) ) );