fmod SET is
  protecting NAT .

  sort NatSet .
  subsort Nat < NatSet .

  op nil : -> NatSet [ctor].
  op _;_ : NatSet NatSet -> NatSet
    [ctor assoc comm id: nil].
  
  var N        : Nat .
  var Set Set' : NatSet .

  eq N ; N = N .

  --- member(2, (1 + 1) ; 3) .
  op member : Nat NatSet -> Bool .
  eq member(N, N ; Set) = true .
  eq member(N, Set) = false [owise].

  op subset : NatSet NatSet -> Bool .
  ceq subset(N ; Set, Set') = false
   if not member(N, Set') .
  eq subset(Set, Set') = true [owise].
endfm