let r, s, t, x be Real; :: thesis: for XT being Subset of REAL st 0 < t & r <= x & x <= s & XT = ].(x - t),(x + t).[ /\ [.r,s.] holds
( ( r <= x - t & x + t <= s implies ( lower_bound XT = x - t & upper_bound XT = x + t ) ) & ( r <= x - t & s < x + t implies ( lower_bound XT = x - t & upper_bound XT = s ) ) & ( x - t < r & x + t <= s implies ( lower_bound XT = r & upper_bound XT = x + t ) ) & ( x - t < r & s < x + t implies ( lower_bound XT = r & upper_bound XT = s ) ) )
let XT be Subset of REAL; :: thesis: ( 0 < t & r <= x & x <= s & XT = ].(x - t),(x + t).[ /\ [.r,s.] implies ( ( r <= x - t & x + t <= s implies ( lower_bound XT = x - t & upper_bound XT = x + t ) ) & ( r <= x - t & s < x + t implies ( lower_bound XT = x - t & upper_bound XT = s ) ) & ( x - t < r & x + t <= s implies ( lower_bound XT = r & upper_bound XT = x + t ) ) & ( x - t < r & s < x + t implies ( lower_bound XT = r & upper_bound XT = s ) ) ) )
assume that
A1: 0 < t and
A2: ( r <= x & x <= s ) and
A3: XT = ].(x - t),(x + t).[ /\ [.r,s.] ; :: thesis: ( ( r <= x - t & x + t <= s implies ( lower_bound XT = x - t & upper_bound XT = x + t ) ) & ( r <= x - t & s < x + t implies ( lower_bound XT = x - t & upper_bound XT = s ) ) & ( x - t < r & x + t <= s implies ( lower_bound XT = r & upper_bound XT = x + t ) ) & ( x - t < r & s < x + t implies ( lower_bound XT = r & upper_bound XT = s ) ) )
hereby :: thesis: ( ( r <= x - t & s < x + t implies ( lower_bound XT = x - t & upper_bound XT = s ) ) & ( x - t < r & x + t <= s implies ( lower_bound XT = r & upper_bound XT = x + t ) ) & ( x - t < r & s < x + t implies ( lower_bound XT = r & upper_bound XT = s ) ) )
assume that
A4: r <= x - t and
A5: x + t <= s ; :: thesis: ( lower_bound XT = x - t & upper_bound XT = x + t )
( x - t < x - 0 & x + 0 < x + t ) by A1, XREAL_1:15, XREAL_1:8;
then A6: x - t < x + t by XXREAL_0:2;
XT = ].(x - t),(x + t).[ by A3, A4, A5, Th42;
hence ( lower_bound XT = x - t & upper_bound XT = x + t ) by A6, TOPREAL6:17; :: thesis: verum
end;
hereby :: thesis: ( ( x - t < r & x + t <= s implies ( lower_bound XT = r & upper_bound XT = x + t ) ) & ( x - t < r & s < x + t implies ( lower_bound XT = r & upper_bound XT = s ) ) )
assume that
A7: r <= x - t and
A8: s < x + t ; :: thesis: ( lower_bound XT = x - t & upper_bound XT = s )
A9: x - t < s - 0 by A2, A1, XREAL_1:15;
XT = ].(x - t),s.] by A3, A7, A8, Th42;
hence ( lower_bound XT = x - t & upper_bound XT = s ) by A9, RCOMP_3:6, RCOMP_3:7; :: thesis: verum
end;
hereby :: thesis: ( x - t < r & s < x + t implies ( lower_bound XT = r & upper_bound XT = s ) )
assume that
A10: x - t < r and
A11: x + t <= s ; :: thesis: ( lower_bound XT = r & upper_bound XT = x + t )
A12: r + 0 < x + t by A2, A1, XREAL_1:8;
XT = [.r,(x + t).[ by A10, A11, A3, Th42;
hence ( lower_bound XT = r & upper_bound XT = x + t ) by A12, RCOMP_3:4, RCOMP_3:5; :: thesis: verum
end;
assume that
A13: x - t < r and
A14: s < x + t ; :: thesis: ( lower_bound XT = r & upper_bound XT = s )
A15: r <= s by A2, XXREAL_0:2;
XT = [.r,s.] by A3, A13, A14, Th42;
hence ( lower_bound XT = r & upper_bound XT = s ) by A15, JORDAN5A:19; :: thesis: verum