max_upto[N: nat]: THEORY EXPORTING ALL BEGIN IMPORTING min_lem S: VAR (nonempty?[upto[N]]) n,a,x: VAR upto[N] max(S): {a: upto[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_upto