let X be interval Subset of REAL; :: thesis: ( X is empty or X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
assume not X is empty ; :: thesis: ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then reconsider X = X as non empty interval Subset of REAL ;
per cases ( X is real-bounded or not X is real-bounded ) ;
suppose X is real-bounded ; :: thesis: ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then reconsider X = X as non empty real-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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then consider x being object such that
A1: X = {x} by ZFMISC_1:131;
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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) ) ; :: thesis: verum
end;
suppose not X is trivial ; :: thesis: ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then ex p, q being object st
( p in X & q in X & p <> q ) ;
then A2: lower_bound X < upper_bound X by SEQ_4:12;
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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then X = [.(lower_bound X),(upper_bound X).] by Th13;
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real 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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then X = ].(lower_bound X),(upper_bound X).] by Th15;
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real 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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then X = [.(lower_bound X),(upper_bound X).[ by Th17;
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real 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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then X = ].(lower_bound X),(upper_bound X).[ by Th19;
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) ) by A2; :: thesis: verum
end;
end;
end;
end;
end;
suppose A3: not X is real-bounded ; :: thesis: ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real 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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real 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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then X = left_closed_halfline (upper_bound X) by A4, Th21;
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) ) ; :: thesis: verum
end;
suppose not upper_bound X in X ; :: thesis: ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then X = left_open_halfline (upper_bound X) by A4, Th23;
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real 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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real 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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then X = right_closed_halfline (lower_bound X) by A5, Th25;
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) ) ; :: thesis: verum
end;
suppose not lower_bound X in X ; :: thesis: ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
then X = right_open_halfline (lower_bound X) by A5, Th27;
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real 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 st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
hence ( X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) ) by Th28; :: thesis: verum
end;
end;
end;
end;