let M be non empty MetrSpace; :: thesis: for P being Subset of (TopSpaceMetr M)
for x being Point of M st x in P holds
0 in (dist x) .: P
let P be Subset of (TopSpaceMetr M); :: thesis: for x being Point of M st x in P holds
0 in (dist x) .: P
let x be Point of M; :: thesis: ( x in P implies 0 in (dist x) .: P )
A1: dom (dist x) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
assume x in P ; :: thesis: 0 in (dist x) .: P
then (dist x) . x in (dist x) .: P by A1, FUNCT_1:def 6;
hence 0 in (dist x) .: P by Th2; :: thesis: verum