:: deftheorem Def7 defines inf XXREAL_2:def 7 :
for X being ext-real-membered left_end set
for b₂ being ExtReal holds
( b₂ = inf X iff ( b₂ in X & ( for x being ExtReal st x in X holds
b₂ <= x ) ) );