let X be interval Subset of REAL; :: thesis: ( X is empty or X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )
assume not X is empty ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )
then reconsider X = X as non empty interval Subset of REAL ;

per cases ( X is bounded or not X is bounded ) ;

suppose X is bounded ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then reconsider X = X as non empty bounded interval Subset of REAL ;

per cases ( X is trivial or not X is trivial ) ;

suppose X is trivial ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then consider x being set such that
A1: X = {x} by REALSET1:def 4;
x in X by A1, TARSKI:def 1;
then reconsider x = x as Real ;
X = [.x,x.] by A1, XXREAL_1:17;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) ; :: thesis: verum

end;

suppose not X is trivial ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then ex p, q being set st
( p in X & q in X & p <> q ) by REALSET1:14;
then A2: lower_bound X < upper_bound X by SEQ_4:25;

per cases ( ( upper_bound X in X & lower_bound X in X ) or ( upper_bound X in X & not lower_bound X in X ) or ( not upper_bound X in X & lower_bound X in X ) or ( not upper_bound X in X & not lower_bound X in X ) ) ;

suppose ( upper_bound X in X & lower_bound X in X ) ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then X = [.(lower_bound X),(upper_bound X).] by Th25;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) by A2; :: thesis: verum

end;

suppose ( upper_bound X in X & not lower_bound X in X ) ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then X = ].(lower_bound X),(upper_bound X).] by Th27;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) by A2; :: thesis: verum

end;

suppose ( not upper_bound X in X & lower_bound X in X ) ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then X = [.(lower_bound X),(upper_bound X).[ by Th29;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) by A2; :: thesis: verum

end;

suppose ( not upper_bound X in X & not lower_bound X in X ) ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then X = ].(lower_bound X),(upper_bound X).[ by Th31;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) by A2; :: thesis: verum

end;

end;

end;

end;

end;

suppose A3: not X is bounded ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

per cases ( ( not X is bounded_below & X is bounded_above ) or ( not X is bounded_above & X is bounded_below ) or ( not X is bounded_above & not X is bounded_below ) ) by A3;

suppose A4: ( not X is bounded_below & X is bounded_above ) ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

per cases ( upper_bound X in X or not upper_bound X in X ) ;

suppose upper_bound X in X ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then X = left_closed_halfline (upper_bound X) by A4, Th33;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) ; :: thesis: verum

end;

suppose not upper_bound X in X ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then X = left_open_halfline (upper_bound X) by A4, Th35;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) ; :: thesis: verum

end;

end;

end;

suppose A5: ( not X is bounded_above & X is bounded_below ) ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

per cases ( lower_bound X in X or not lower_bound X in X ) ;

suppose lower_bound X in X ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then X = right_closed_halfline (lower_bound X) by A5, Th37;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) ; :: thesis: verum

end;

suppose not lower_bound X in X ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

then X = right_open_halfline (lower_bound X) by A5, Th39;
hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) ; :: thesis: verum

end;

end;

end;

suppose ( not X is bounded_above & not X is bounded_below ) ; :: thesis: ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

hence ( X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) by Th40; :: thesis: verum

end;

end;

end;

end;