let n be Nat; :: thesis: for r being Real
for A being non empty Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) st q in A holds
dist (p,q) >= r ) holds
dist (p,A) >= r
let r be Real; :: thesis: for A being non empty Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) st q in A holds
dist (p,q) >= r ) holds
dist (p,A) >= r
let A be non empty Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) st q in A holds
dist (p,q) >= r ) holds
dist (p,A) >= r
let p9 be Point of (TOP-REAL n); :: thesis: ( ( for q being Point of (TOP-REAL n) st q in A holds
dist (p9,q) >= r ) implies dist (p9,A) >= r )
assume A1: for q being Point of (TOP-REAL n) st q in A holds
dist (p9,q) >= r ; :: thesis: dist (p9,A) >= r
for p, q being Point of (TOP-REAL n) st p in {p9} & q in A holds
dist (p,q) >= r
proof
let p, q be Point of (TOP-REAL n); :: thesis: ( p in {p9} & q in A implies dist (p,q) >= r )
assume that
A2: p in {p9} and
A3: q in A ; :: thesis: dist (p,q) >= r
p = p9 by A2, TARSKI:def 1;
hence dist (p,q) >= r by A1, A3; :: thesis: verum
end;
hence dist (p9,A) >= r by Th40; :: thesis: verum