:: deftheorem Def2 defines least-positive FVALUAT1:def 2 :
for X being ext-real-membered set st ex i0 being positive ExtInt st i0 in X holds
for b₂ being positive ExtInt holds
( b₂ = least-positive X iff ( b₂ in X & ( for i being positive ExtInt st i in X holds
b₂ <= i ) ) );