let r, s be Real; :: thesis: for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is connected
let jauge be Function of [.r,s.],].0,+infty.[; :: thesis: for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is connected
let S be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis: ( S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } implies S is connected )
assume A1: S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } ; :: thesis: S is connected
for X being Subset of (Closed-Interval-TSpace (r,s)) st X in S holds
X is connected
proof
let X be Subset of (Closed-Interval-TSpace (r,s)); :: thesis: ( X in S implies X is connected )
assume X in S ; :: thesis: X is connected
then consider x0 being Element of [.r,s.] such that
A2: X = ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ /\ [.r,s.] by A1;
thus X is connected by A2, RCOMP_3:43; :: thesis: verum
end;
hence S is connected by RCOMP_3:def 1; :: thesis: verum