let r, s be Real; :: thesis: 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))
let jauge be Function of [.r,s.],].0,+infty.[; :: thesis: ( r <= s implies { (].(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)) )
assume A1: r <= s ; :: thesis: { (].(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))
set A = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } ;
{ (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } c= bool [.r,s.]

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } or t in bool [.r,s.] )
assume t in { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } ; :: thesis: t in bool [.r,s.]
then consider x0 being Element of [.r,s.] such that
A2: t = ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ /\ [.r,s.] ;
reconsider t = t as set by TARSKI:1;
t c= [.r,s.] by A2, XBOOLE_1:17;
hence t in bool [.r,s.] ; :: thesis: verum

end;

hence { (].(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)) by A1, TOPMETR:18; :: thesis: verum