let I be non empty Interval; :: thesis: ( not sup I in I or I = [.(inf I),(sup I).] or I = ].(inf I),(sup I).] )
assume sup 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:3, XXREAL_1:4;
hence ( I = [.(inf I),(sup I).] or I = ].(inf I),(sup I).] ) by Lm22; :: thesis: verum