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 r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is Cover of (Closed-Interval-TSpace (r,s))
let jauge be Function of [.r,s.],].0,+infty.[; :: thesis: for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is Cover of (Closed-Interval-TSpace (r,s))
let S be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis: ( r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } implies S is Cover of (Closed-Interval-TSpace (r,s)) )
assume that
A1: r <= s and
A2: S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } ; :: thesis: S is Cover of (Closed-Interval-TSpace (r,s))
[.r,s.] c= union S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.r,s.] or x in union S )
assume A3: x in [.r,s.] ; :: thesis: x in union S
then reconsider x0 = x as Element of [.r,s.] ;
x0 in dom jauge by A3, PARTFUN1:def 2;
then jauge . x0 in rng jauge by FUNCT_1:3;
then 0 < jauge . x0 by XXREAL_1:4;
then ( x0 - (jauge . x0) < x0 - 0 & x0 + 0 < x0 + (jauge . x0) ) by XREAL_1:15, XREAL_1:8;
then x0 in ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ by XXREAL_1:4;
then A5: x0 in ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ /\ [.r,s.] by A3, XBOOLE_0:def 4;
].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ /\ [.r,s.] in S by A2;
hence x in union S by A5, TARSKI:def 4; :: thesis: verum

end;

then S is Cover of [.r,s.] by SETFAM_1:def 11;
hence S is Cover of (Closed-Interval-TSpace (r,s)) by A1, TOPMETR:18; :: thesis: verum