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 ) )
;

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;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

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;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

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;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

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;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