:: deftheorem defines with_min MEASURE6:def 5 :
for X being real-membered set holds
( X is with_min iff ( X is bounded_below & lower_bound X in X ) );