let n be Element of 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 p' be Point of (TOP-REAL n); :: thesis: ( ( for q being Point of (TOP-REAL n) st q in A holds
dist p',q >= r ) implies dist p',A >= r )
assume A1: for q being Point of (TOP-REAL n) st q in A holds
dist p',q >= r ; :: thesis: dist p',A >= r
for p, q being Point of (TOP-REAL n) st p in {p'} & q in A holds
dist p,q >= r

proof

let p, q be Point of (TOP-REAL n); :: thesis: ( p in {p'} & q in A implies dist p,q >= r )
assume that
A2: p in {p'} and
A3: q in A ; :: thesis: dist p,q >= r
p = p' by A2, TARSKI:def 1;
hence dist p,q >= r by A1, A3; :: thesis: verum

end;

hence dist p',A >= r by Th40; :: thesis: verum