for C being non void Signature
for o being OperSymbol of C holds
( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) ) ;