set S = the op-discrete OrderSortedSign;
take the op-discrete OrderSortedSign ; :: thesis: the op-discrete OrderSortedSign is monotone
thus the op-discrete OrderSortedSign is monotone by Th9; :: thesis: verum