let n be Nat; :: thesis: for r, s being Real
for e being Point of (Euclid n) st r <= s holds
OpenHypercube (e,r) c= OpenHypercube (e,s)
let r, s be Real; :: 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 :: thesis: for x being object st x in dom (Intervals (e,r)) holds
(Intervals (e,r)) . x c= (Intervals (e,s)) . x
let x be object ; :: 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 ;
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:6, XREAL_1:10;
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:27; :: thesis: verum