let I be non empty Interval; :: thesis: ( I = [.(inf I),(sup I).] or I = ].(inf I),(sup I).] or I = [.(inf I),(sup I).[ or I = ].(inf I),(sup I).[ )
( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by MEASURE5:1;
hence ( I = [.(inf I),(sup I).] or I = ].(inf I),(sup I).] or I = [.(inf I),(sup I).[ or I = ].(inf I),(sup I).[ ) by MEASURE6:16, MEASURE6:17, MEASURE6:18, MEASURE6:19; :: thesis: verum