let M be non empty MetrSpace; :: thesis: for P being Subset of (TopSpaceMetr M)
for x being Point of M
for y being real number 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 number st y in (dist x) .: P holds
y >= 0
let x be Point of M; :: thesis: for y being real number st y in (dist x) .: P holds
y >= 0
let y be real number ; :: thesis: ( y in (dist x) .: P implies y >= 0 )
assume y in (dist x) .: P ; :: thesis: y >= 0
then consider z being set such that
z in dom (dist x) and
A1: z in P and
A2: y = (dist x) . z by FUNCT_1:def 12;
reconsider z' = z as Point of M by A1, TOPMETR:16;
y = dist x,z' by A2, WEIERSTR:def 6;
hence y >= 0 by METRIC_1:5; :: thesis: verum