set o = the OperSymbol of S;
take the OperSymbol of S ; :: thesis: the OperSymbol of S is monotone
thus the OperSymbol of S is monotone by Def9; :: thesis: verum