let q4, q, p2 be Point of (TOP-REAL 2); :: thesis: for O, u, uq being Point of (Euclid 2) st u in cl_Ball O,(|.p2.| + 1) & q = uq & q4 = u & O = 0. (TOP-REAL 2) & |.q4.| = |.q.| holds
q in cl_Ball O,(|.p2.| + 1)
let O, u, uq be Point of (Euclid 2); :: thesis: ( u in cl_Ball O,(|.p2.| + 1) & q = uq & q4 = u & O = 0. (TOP-REAL 2) & |.q4.| = |.q.| implies q in cl_Ball O,(|.p2.| + 1) )
assume A1: u in cl_Ball O,(|.p2.| + 1) ; :: thesis: ( not q = uq or not q4 = u or not O = 0. (TOP-REAL 2) or not |.q4.| = |.q.| or q in cl_Ball O,(|.p2.| + 1) )
assume that
A2: q = uq and
A3: q4 = u and
A4: O = 0. (TOP-REAL 2) ; :: thesis: ( not |.q4.| = |.q.| or q in cl_Ball O,(|.p2.| + 1) )
assume A5: |.q4.| = |.q.| ; :: thesis: q in cl_Ball O,(|.p2.| + 1)

now

assume not q in cl_Ball O,(|.p2.| + 1) ; :: thesis: contradiction
then not dist O,uq <= |.p2.| + 1 by A2, METRIC_1:13;
then |.((0. (TOP-REAL 2)) - q).| > |.p2.| + 1 by A2, A4, JGRAPH_1:45;
then |.(- q).| > |.p2.| + 1 by EUCLID:31;
then |.q.| > |.p2.| + 1 by TOPRNS_1:27;
then |.(- q4).| > |.p2.| + 1 by A5, TOPRNS_1:27;
then |.((0. (TOP-REAL 2)) - q4).| > |.p2.| + 1 by EUCLID:31;
then dist O,u > |.p2.| + 1 by A3, A4, JGRAPH_1:45;
hence contradiction by A1, METRIC_1:13; :: thesis: verum

end;

hence q in cl_Ball O,(|.p2.| + 1) ; :: thesis: verum