theorem :: COUSIN:53

for r, s being Real
for jauge being Function of [.r,s.],].0,+infty.[ st r <= s holds
{ (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } is Subset-Family of (Closed-Interval-TSpace (r,s))