let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r, s being Real st r < s holds
ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s)
let p be Point of (TOP-REAL n); :: thesis: for r, s being Real st r < s holds
ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s)
let r, s be Real; :: thesis: ( r < s implies ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s) )
assume A1: r < s ; :: thesis: ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ClosedHypercube (p,(n |-> r)) or x in OpenHypercube (p,s) )
assume A2: x in ClosedHypercube (p,(n |-> r)) ; :: thesis: x in OpenHypercube (p,s)
reconsider q = x as Point of (TOP-REAL n) by A2;

now :: thesis: for i being Nat st i in Seg n holds
q . i in ].((p . i) - s),((p . i) + s).[

let i be Nat; :: thesis: ( i in Seg n implies q . i in ].((p . i) - s),((p . i) + s).[ )
assume A3: i in Seg n ; :: thesis: q . i in ].((p . i) - s),((p . i) + s).[
(n |-> r) . i = r by A3, FINSEQ_2:57;
then A4: q . i in [.((p . i) - r),((p . i) + r).] by A2, A3, Def2;
A5: (p . i) + r < (p . i) + s by A1, XREAL_1:6;
q . i <= (p . i) + r by A4, XXREAL_1:1;
then A6: q . i < (p . i) + s by A5, XXREAL_0:2;
A7: (p . i) - r > (p . i) - s by A1, XREAL_1:10;
q . i >= (p . i) - r by A4, XXREAL_1:1;
then q . i > (p . i) - s by A7, XXREAL_0:2;
hence q . i in ].((p . i) - s),((p . i) + s).[ by A6, XXREAL_1:4; :: thesis: verum

end;

hence x in OpenHypercube (p,s) by Th3; :: thesis: verum