:: deftheorem Def5 defines left_end XXREAL_2:def 5 :
for X being ext-real-membered set holds
( X is left_end iff inf X in X );