:: deftheorem Def4 defines inf XXREAL_2:def 4 :
for X being ext-real-membered set
for b₂ being ExtReal holds
( b₂ = inf X iff ( b₂ is LowerBound of X & ( for x being LowerBound of X holds x <= b₂ ) ) );