let I be interval Subset of REAL; :: thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval )

per cases ( ( I is left_end & I is right_end ) or ( not I is left_end & I is right_end ) or ( I is left_end & not I is right_end ) or ( not I is left_end & not I is right_end ) ) ;

suppose A1: ( I is left_end & I is right_end ) ; :: thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval )

reconsider a = inf I, b = sup I as R_eal ;
A2: ( a in I & I = [.a,b.] ) by A1, XXREAL_2:75, 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 A1, A2; :: thesis: verum

end;

suppose A3: ( not I is left_end & I is right_end ) ; :: thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval )

set a = inf I;
set b = sup I;
A4: I = ].(inf I),(sup I).] by A3, XXREAL_2:76;
A5: sup I in I by A3, 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 A5, A4; :: thesis: verum

end;

suppose A6: ( I is left_end & not I is right_end ) ; :: thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval )

set a = inf I;
set b = sup I;
A7: I = [.(inf I),(sup I).[ by A6, XXREAL_2:77;
A8: inf I in I by A6, 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 A8, A7; :: thesis: verum

end;

suppose ( not I is left_end & not I is right_end ) ; :: thesis: ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval )

then consider a, b being ExtReal such that
A9: a <= b and
A10: I = ].a,b.[ by XXREAL_2:79;
reconsider a = a, b = b as R_eal by XXREAL_0:def 1;
a <= b by A9;
hence ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by A10; :: thesis: verum

end;

end;