consider S being op-discrete OrderSortedSign;
take S ; :: thesis: S is monotone
thus S is monotone by Th9; :: thesis: verum