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 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 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 st q = q2 holds
Ball (q2,r) = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }
let r be Real; :: 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 object ; :: 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:8;
dist (q2,q4) = |.(q - q44).| by A1, JGRAPH_1:28;
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 object ; :: 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:8;
dist (q2,q34) = |.(q - q3).| by A1, JGRAPH_1:28;
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:17;
hence Ball (q2,r) = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r } by A2, A4; :: thesis: verum