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 :: thesis: q in cl_Ball (O,(|.p2.| + 1))
assume not q in cl_Ball (O,(|.p2.| + 1)) ; :: thesis: contradiction
then not dist (O,uq) <= |.p2.| + 1 by A2, METRIC_1:12;
then |.((0. (TOP-REAL 2)) - q).| > |.p2.| + 1 by A2, A4, JGRAPH_1:28;
then |.(- q).| > |.p2.| + 1 by RLVECT_1:4;
then |.q.| > |.p2.| + 1 by TOPRNS_1:26;
then |.(- q4).| > |.p2.| + 1 by A5, TOPRNS_1:26;
then |.((0. (TOP-REAL 2)) - q4).| > |.p2.| + 1 by RLVECT_1:4;
then dist (O,u) > |.p2.| + 1 by A3, A4, JGRAPH_1:28;
hence contradiction by A1, METRIC_1:12; :: thesis: verum
end;
hence q in cl_Ball (O,(|.p2.| + 1)) ; :: thesis: verum