let I be interval Subset of REAL; :: thesis: ( inf I in I implies inf I = lower_bound I )
assume inf I in I ; :: thesis: inf I = lower_bound I
then reconsider J = I as non empty real-membered left_end set by XXREAL_2:def 5;
inf J = lower_bound J ;
hence inf I = lower_bound I ; :: thesis: verum