theorem :: COUSIN:59

for r, s, t, x being Real
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 ) ) )