let n be Element of NAT ; :: thesis: for q2 being Point of (Euclid n)
for q being Point of (TOP-REAL n)
for r being real number st q = q2 holds
Ball q2,r = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }
let q2 be Point of (Euclid n); :: thesis: for q being Point of (TOP-REAL n)
for r being real number st q = q2 holds
Ball q2,r = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }
let q be Point of (TOP-REAL n); :: thesis: for r being real number st q = q2 holds
Ball q2,r = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }
let r be real number ; :: thesis: ( q = q2 implies Ball q2,r = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r } )
assume A1: q = q2 ; :: thesis: Ball q2,r = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }
A2: { q4 where q4 is Element of (Euclid n) : dist q2,q4 < r } c= { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q4 where q4 is Element of (Euclid n) : dist q2,q4 < r } or x in { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r } )
assume x in { q4 where q4 is Element of (Euclid n) : dist q2,q4 < r } ; :: thesis: x in { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }
then consider q4 being Element of (Euclid n) such that
A3: ( q4 = x & dist q2,q4 < r ) ;
reconsider q44 = q4 as Point of (TOP-REAL n) by TOPREAL3:13;
dist q2,q4 = |.(q - q44).| by A1, JGRAPH_1:45;
hence x in { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r } by A3; :: thesis: verum

end;

A4: { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r } c= { q4 where q4 is Element of (Euclid n) : dist q2,q4 < r }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r } or x in { q4 where q4 is Element of (Euclid n) : dist q2,q4 < r } )
assume x in { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r } ; :: thesis: x in { q4 where q4 is Element of (Euclid n) : dist q2,q4 < r }
then consider q3 being Point of (TOP-REAL n) such that
A5: ( x = q3 & |.(q - q3).| < r ) ;
reconsider q34 = q3 as Point of (Euclid n) by TOPREAL3:13;
dist q2,q34 = |.(q - q3).| by A1, JGRAPH_1:45;
hence x in { q4 where q4 is Element of (Euclid n) : dist q2,q4 < r } by A5; :: thesis: verum

end;

Ball q2,r = { q4 where q4 is Element of (Euclid n) : dist q2,q4 < r } by METRIC_1:18;
hence Ball q2,r = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r } by A2, A4, XBOOLE_0:def 10; :: thesis: verum