let I be non empty Interval; :: thesis: ( not sup I in I or I is closed_interval or I is left_open_interval )
assume A1: sup I in I ; :: thesis: ( I is closed_interval or I is left_open_interval )

A2: now :: thesis: not I is open_interval

assume I is open_interval ; :: thesis: contradiction
then consider a, b being R_eal such that
A3: I = ].a,b.[ by MEASURE5:def 2;
sup I = b by A3, XXREAL_1:28, XXREAL_2:32;
hence contradiction by A1, A3, XXREAL_1:4; :: thesis: verum

end;

now :: thesis: not I is right_open_interval

assume I is right_open_interval ; :: thesis: contradiction
then consider a being Real, b being R_eal such that
A4: I = [.a,b.[ by MEASURE5:def 4;
sup I = b by A4, XXREAL_1:27, XXREAL_2:31;
hence contradiction by A1, A4, XXREAL_1:3; :: thesis: verum

end;

hence ( I is closed_interval or I is left_open_interval ) by A2, MEASURE5:1; :: thesis: verum