theorem Th42: :: COUSIN:58

for r, s, t, x being Real holds
( ( r <= x - t & x + t <= s implies ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),(x + t).[ ) & ( r <= x - t & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),s.] ) & ( x - t < r & x + t <= s implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[ ) & ( x - t < r & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.] ) )