for S being OrderSortedSign
for X being set holds
( X is OperName of S iff ex op1 being OperSymbol of S st X = Name op1 )