min_lem: THEORY BEGIN S: VAR (nonempty?[nat]) min_lem : LEMMA minimum?(min(S), S) END min_lem