let n be Nat; :: thesis: for r, s being real number
for e being Point of (Euclid n) st r <= s holds
OpenHypercube e,r c= OpenHypercube e,s
let r, s be real number ; :: thesis: for e being Point of (Euclid n) st r <= s holds
OpenHypercube e,r c= OpenHypercube e,s
let e be Point of (Euclid n); :: thesis: ( r <= s implies OpenHypercube e,r c= OpenHypercube e,s )
assume A1: r <= s ; :: thesis: OpenHypercube e,r c= OpenHypercube e,s
A2: dom (Intervals e,s) = dom e by Def3;
A3: dom (Intervals e,r) = dom e by Def3;

now

let x be set ; :: thesis: ( x in dom (Intervals e,r) implies (Intervals e,r) . x c= (Intervals e,s) . x )
assume A4: x in dom (Intervals e,r) ; :: thesis: (Intervals e,r) . x c= (Intervals e,s) . x
reconsider u = e . x as real number ;
A5: ( (Intervals e,r) . x = ].(u - r),(u + r).[ & (Intervals e,s) . x = ].(u - s),(u + s).[ ) by A4, A3, Def3;
( u - s <= u - r & u + r <= u + s ) by A1, XREAL_1:8, XREAL_1:12;
hence (Intervals e,r) . x c= (Intervals e,s) . x by A5, XXREAL_1:46; :: thesis: verum

end;

hence OpenHypercube e,r c= OpenHypercube e,s by A2, A3, CARD_3:38; :: thesis: verum