let I be non empty Interval; :: thesis: ( not inf I in I or I = [.(inf I),(sup I).] or I = [.(inf I),(sup I).[ )
assume inf I in I ; :: thesis: ( I = [.(inf I),(sup I).] or I = [.(inf I),(sup I).[ )
then ( not I = ].(inf I),(sup I).] & not I = ].(inf I),(sup I).[ ) by XXREAL_1:2, XXREAL_1:4;
hence ( I = [.(inf I),(sup I).] or I = [.(inf I),(sup I).[ ) by Lm22; :: thesis: verum