let x be Element of o; :: thesis: x is OperSymbol of S
thus x is OperSymbol of S ; :: thesis: verum