THEORY Monoid
  TYPE PARAMETERS M
  OPERATORS
    associative predicate (op: (M * M) --> M)
      direct definition 
        ! x, y, z . x : M & y : M & z : M => op(x |-> op(y |-> z)) = op(op(x |-> y) |-> z)
    neutral predicate (op: (M * M) --> M,e: M)
      well-definedness M /= {}
      direct definition 
        ! x . x : M => (op(x |-> e) = x & op(e |-> x) = x)
    Monoid predicate (op: (M * M) --> M,e: M)
      well-definedness M /= {}
      direct definition 
        associative(op) & neutral(op, e)
  THEOREMS
    neutralUnicity: 
      ! op, e . op : ((M * M) --> M) & e : M & Monoid(op, e) => (
        ! x . x : M & neutral(op, x) => x = e
      )
END