let r be Real; :: thesis: for X being non empty interval Subset of REAL holds
( r in X or r <= lower_bound X or upper_bound X <= r )
let X be non empty interval Subset of REAL; :: thesis: ( r in X or r <= lower_bound X or upper_bound X <= r )
assume A1: not r in X ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
per cases ( 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 Th29;
suppose X = REAL ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, XREAL_0:def 1; :: thesis: verum
end;
suppose ex a being Real st X = left_closed_halfline a ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
then consider a being Real such that
A2: X = left_closed_halfline a ;
upper_bound X = a by A2, Th9;
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, A2, XXREAL_1:234; :: thesis: verum
end;
suppose ex a being Real st X = left_open_halfline a ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
then consider a being Real such that
A3: X = left_open_halfline a ;
upper_bound X = a by A3, Th10;
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, A3, XXREAL_1:233; :: thesis: verum
end;
suppose ex a being Real st X = right_closed_halfline a ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
then consider a being Real such that
A4: X = right_closed_halfline a ;
lower_bound X = a by A4, Th11;
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, A4, XXREAL_1:236; :: thesis: verum
end;
suppose ex a being Real st X = right_open_halfline a ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
then consider a being Real such that
A5: X = right_open_halfline a ;
lower_bound X = a by A5, Th12;
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, A5, XXREAL_1:235; :: thesis: verum
end;
suppose ex a, b being Real st
( a <= b & X = [.a,b.] ) ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
then consider a, b being Real such that
A6: a <= b and
A7: X = [.a,b.] ;
( lower_bound X = a & upper_bound X = b ) by A6, A7, JORDAN5A:19;
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, A7, XXREAL_1:1; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & X = [.a,b.[ ) ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
then consider a, b being Real such that
A8: a < b and
A9: X = [.a,b.[ ;
( lower_bound X = a & upper_bound X = b ) by A8, A9, Th4, Th5;
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, A9, XXREAL_1:3; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & X = ].a,b.] ) ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
then consider a, b being Real such that
A10: a < b and
A11: X = ].a,b.] ;
( lower_bound X = a & upper_bound X = b ) by A10, A11, Th6, Th7;
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, A11, XXREAL_1:2; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & X = ].a,b.[ ) ; :: thesis: ( r <= lower_bound X or upper_bound X <= r )
then consider a, b being Real such that
A12: a < b and
A13: X = ].a,b.[ ;
( lower_bound X = a & upper_bound X = b ) by A12, A13, TOPREAL6:17;
hence ( r <= lower_bound X or upper_bound X <= r ) by A1, A13, XXREAL_1:4; :: thesis: verum
end;
end;