thus ( not IT is interval or IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) :: thesis: ( ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) implies IT is interval )

proof

assume A1: IT is interval ; :: thesis: ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval )

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

suppose A2: ( IT is left_end & IT is right_end ) ; :: thesis: ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval )

reconsider a = inf IT, b = sup IT as R_eal ;
A3: ( a in IT & IT = [.a,b.] ) by A1, A2, XXREAL_2:79, XXREAL_2:def 5;
then a <= b by XXREAL_1:1;
hence ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) by A2, A3, Def6; :: thesis: verum

end;

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

set a = inf IT;
set b = sup IT;
A5: IT = ].(inf IT),(sup IT).] by A1, A4, XXREAL_2:80;
A6: sup IT in IT by A4, XXREAL_2:def 6;
then inf IT <= sup IT by XXREAL_2:40;
hence ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) by A6, A5, Def8; :: thesis: verum

end;

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

set a = inf IT;
set b = sup IT;
A8: IT = [.(inf IT),(sup IT).[ by A1, A7, XXREAL_2:81;
A9: inf IT in IT by A7, XXREAL_2:def 5;
then inf IT <= sup IT by XXREAL_2:40;
hence ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) by A9, A8, Def7; :: thesis: verum

end;

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

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

end;

end;

end;

assume A12: ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) ; :: thesis: IT is interval

per cases ( IT is open_interval or IT is closed_interval or IT is left_open_interval or IT is right_open_interval ) by A12;

suppose IT is open_interval ; :: thesis: IT is interval

then ex a, b being R_eal st
( a <= b & IT = ].a,b.[ ) by Def5;
hence IT is interval ; :: thesis: verum

end;

suppose IT is closed_interval ; :: thesis: IT is interval

then ex a, b being real number st
( a <= b & IT = [.a,b.] ) by Def6;
hence IT is interval ; :: thesis: verum

end;

suppose IT is left_open_interval ; :: thesis: IT is interval

then ex a being R_eal ex b being real number st
( a <= b & IT = ].a,b.] ) by Def8;
hence IT is interval ; :: thesis: verum

end;

suppose IT is right_open_interval ; :: thesis: IT is interval

then ex a being real number ex b being R_eal st
( a <= b & IT = [.a,b.[ ) by Def7;
hence IT is interval ; :: thesis: verum

end;

end;