max_below[N: nat]: THEORY

  EXPORTING ALL

BEGIN

  IMPORTING min_nat

  S: VAR (nonempty?[below[N]])
  n,a,x: VAR below[N]

  max(S): {a: below[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}

  maximum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a >= x)

  max_def         : LEMMA max(S) = a IFF maximum?(a, S)

  max_lem         : LEMMA maximum?(max(S), S)

END max_below