let I be non empty Interval; :: thesis: ( not inf I in I or I is closed_interval or I is right_open_interval )
assume A1: inf I in I ; :: thesis: ( I is closed_interval or I is right_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;
inf I = a by A3, XXREAL_1:28, XXREAL_2:28;
hence contradiction by A1, A3, XXREAL_1:4; :: thesis: verum

end;

now :: thesis: not I is left_open_interval

assume I is left_open_interval ; :: thesis: contradiction
then consider a being R_eal, b being Real such that
A4: I = ].a,b.] by MEASURE5:def 5;
inf I = a by A4, XXREAL_1:26, XXREAL_2:27;
hence contradiction by A1, A4, XXREAL_1:2; :: thesis: verum

end;

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