let I be interval Subset of REAL; :: thesis:

per cases ;

suppose A2: ( I is left_end & I is right_end ) ; :: thesis:

reconsider a = inf I, b = sup I as R_eal ;
A3: ( a in I & I = [.a,b.] ) by A2, XXREAL_2:79, XXREAL_2:def 5;
thus ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A2, A3, Def6; :: thesis:

end;

suppose A4: ( not I is left_end & I is right_end ) ; :: thesis:

set a = inf I;
set b = sup I;
A5: I = ].(inf I),(sup I).] by A4, XXREAL_2:80;
A6: sup I in I by A4, XXREAL_2:def 6;
thus ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A6, A5, Def8; :: thesis:

end;

suppose A7: ( I is left_end & not I is right_end ) ; :: thesis:

set a = inf I;
set b = sup I;
A8: I = [.(inf I),(sup I).[ by A7, XXREAL_2:81;
A9: inf I in I by A7, XXREAL_2:def 5;
thus ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A9, A8, Def7; :: thesis:

end;

suppose ( not I is left_end & not I is right_end ) ; :: thesis:

then consider a, b being ext-real number such that
A10: a <= b and
A11: I = ].a,b.[ by XXREAL_2:83;
reconsider a = a, b = b as R_eal by XXREAL_0:def 1;
a <= b by A10;
hence ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A11, Def5; :: thesis:

end;

end;