for S being OrderSortedSign
for z being non empty set
for z1 being Element of z holds
( TrivialOSA (S,z,z1) is non-empty & TrivialOSA (S,z,z1) is monotone )