:: deftheorem defines with_max MEASURE6:def 4 :
for X being real-membered set holds
( X is with_max iff ( X is bounded_above & upper_bound X in X ) );