the set of ships is nonempty and finite
(any reasonable notion of) size induces a total order on the set of equivalence classes of ships of the same size
every nonempty finite total order has a maximum
there exists a ship that is no smaller than any other ship
QED
putting this on the pre-calc 12 exam





















