let I be non empty Interval; :: thesis: ( not sup I in I & not inf I in I implies I = ].(inf I),(sup I).[ )
assume A1: ( not sup I in I & not inf I in I ) ; :: thesis: I = ].(inf I),(sup I).[
A2: inf I <= sup I by XXREAL_2:40;
A3: ( I = [.(inf I),(sup I).] or I = ].(inf I),(sup I).] or I = [.(inf I),(sup I).[ or I = ].(inf I),(sup I).[ ) by Lm22;
inf I <> sup I by A3, A1, XXREAL_1:1, XXREAL_1:18, XXREAL_1:19, XXREAL_1:20;
then inf I < sup I by A2, XXREAL_0:1;
then ( sup I in ].(inf I),(sup I).] & sup I in [.(inf I),(sup I).] & inf I in [.(inf I),(sup I).[ ) by XXREAL_1:1, XXREAL_1:2, XXREAL_1:3;
hence I = ].(inf I),(sup I).[ by A1, Lm22; :: thesis: verum