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 Z: 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 S: ( 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 ;
W: ( a in IT & b in IT & IT = [.a,b.] ) by S, Z, XXREAL_2:79, XXREAL_2:def 5, XXREAL_2:def 6;
a <= b by W, 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 W, Def6; :: thesis: verum

end;

suppose S: ( 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;
Y: sup IT in IT by S, XXREAL_2:def 6;
then ( inf IT <= sup IT & IT = ].(inf IT),(sup IT).] ) by S, Z, XXREAL_2:40, XXREAL_2:80;
hence ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) by Def8, Y; :: thesis: verum

end;

suppose S: ( 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;
Y: inf IT in IT by S, XXREAL_2:def 5;
then ( inf IT <= sup IT & IT = [.(inf IT),(sup IT).[ ) by S, Z, XXREAL_2:40, XXREAL_2:81;
hence ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) by Def7, Y; :: 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
W: ( a <= b & IT = ].a,b.[ ) by Z, XXREAL_2:83;
reconsider a = a, b = b as R_eal by XXREAL_0:def 1;
a <= b by W;
hence ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval ) by W, Def5; :: thesis: verum

end;

end;

end;

assume Z: ( 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 Z;

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 consider a, b being real number such that
W: ( a <= b & IT = [.a,b.] ) by Def6;
thus IT is interval by W; :: thesis: verum

end;

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

then consider a being R_eal, b being real number such that
W: ( a <= b & IT = ].a,b.] ) by Def8;
thus IT is interval by W; :: thesis: verum

end;

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

then consider a being real number , b being R_eal such that
W: ( a <= b & IT = [.a,b.[ ) by Def7;
thus IT is interval by W; :: thesis: verum

end;

end;