let I be interval Subset of REAL; :: thesis: ( sup I in I implies sup I = upper_bound I )
assume sup I in I ; :: thesis: sup I = upper_bound I
then reconsider J = I as non empty real-membered right_end set by XXREAL_2:def 6;
sup J = upper_bound J ;
hence sup I = upper_bound I ; :: thesis: verum