let n be Nat; 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); for r, s being Real st r < s holds
ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s)
let r, s be Real; ( r < s implies ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s) )
assume A1:
r < s
; ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s)
let x be object ; TARSKI:def 3 ( not x in ClosedHypercube (p,(n |-> r)) or x in OpenHypercube (p,s) )
assume A2:
x in ClosedHypercube (p,(n |-> r))
; x in OpenHypercube (p,s)
reconsider q = x as Point of (TOP-REAL n) by A2;
now for i being Nat st i in Seg n holds
q . i in ].((p . i) - s),((p . i) + s).[let i be
Nat;
( i in Seg n implies q . i in ].((p . i) - s),((p . i) + s).[ )assume A3:
i in Seg n
;
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;
verum end;
hence
x in OpenHypercube (p,s)
by Th3; verum