Define MAX_SET on the empty set to equal 0.

This make the relevant equation

    FINITE s ==> (MAX_SET (e INSERT s) = MAX e (MAX_SET s))