:: deftheorem defines is_local_minimum_of TOPGEN_3:def 3 :
for X being set
for x being Real holds
( x is_local_minimum_of X iff ( x in X & ex y being Real st
( y < x & ].y,x.[ misses X ) ) );