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 Def8; :: thesis: verum