let M be non empty MetrSpace; :: thesis: for P being Subset of (TopSpaceMetr M)
for x being Point of M
for y being Real st y in (dist x) .: P holds
y >= 0
let P be Subset of (TopSpaceMetr M); :: thesis: for x being Point of M
for y being Real st y in (dist x) .: P holds
y >= 0
let x be Point of M; :: thesis: for y being Real st y in (dist x) .: P holds
y >= 0
let y be Real; :: thesis: ( y in (dist x) .: P implies y >= 0 )
assume y in (dist x) .: P ; :: thesis: y >= 0
then consider z being object such that
z in dom (dist x) and
A1: z in P and
A2: y = (dist x) . z by FUNCT_1:def 6;
reconsider z9 = z as Point of M by A1, TOPMETR:12;
y = dist (x,z9) by A2, WEIERSTR:def 4;
hence y >= 0 by METRIC_1:5; :: thesis: verum