consider o being OperSymbol of S;
take o ; :: thesis: o is monotone
thus o is monotone by Def9; :: thesis: verum