set TR = TOP-REAL n;
let H1, H2 be Subset of (TOP-REAL n); :: thesis: ( ( for q being Point of (TOP-REAL n) holds
( q in H1 iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) & ( for q being Point of (TOP-REAL n) holds
( q in H2 iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) implies H1 = H2 )
assume that
A1: for q being Point of (TOP-REAL n) holds
( q in H1 iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) and
A2: for q being Point of (TOP-REAL n) holds
( q in H2 iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ; :: thesis: H1 = H2

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: H2 c= H1

let x be object ; :: thesis: ( x in H1 implies x in H2 )
assume A3: x in H1 ; :: thesis: x in H2
then reconsider q = x as Point of (TOP-REAL n) ;
for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A1, A3;
hence x in H2 by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H2 or x in H1 )
assume A4: x in H2 ; :: thesis: x in H1
then reconsider q = x as Point of (TOP-REAL n) ;
for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A2, A4;
hence x in H1 by A1; :: thesis: verum