let I, J be Subset of REAL; :: thesis: ( J c= I implies ].(inf J),(sup J).[ c= ].(inf I),(sup I).[ )
assume J c= I ; :: thesis: ].(inf J),(sup J).[ c= ].(inf I),(sup I).[
then ( inf I <= inf J & sup J <= sup I ) by XXREAL_2:59, XXREAL_2:60;
hence ].(inf J),(sup J).[ c= ].(inf I),(sup I).[ by XXREAL_1:46; :: thesis: verum