consider x being Point of M;
reconsider f = the carrier of M --> x as Function of M,M ;
take f ; :: thesis: ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds dist ((f . x),(f . y)) <= L * (dist (x,y)) ) )
take 1 / 2 ; :: thesis: ( 0 < 1 / 2 & 1 / 2 < 1 & ( for x, y being Point of M holds dist ((f . x),(f . y)) <= (1 / 2) * (dist (x,y)) ) )
thus ( 0 < 1 / 2 & 1 / 2 < 1 ) ; :: thesis: for x, y being Point of M holds dist ((f . x),(f . y)) <= (1 / 2) * (dist (x,y))
let z, y be Point of M; :: thesis: dist ((f . z),(f . y)) <= (1 / 2) * (dist (z,y))
( f . z = x & f . y = x ) by FUNCOP_1:13;
then A1: dist ((f . z),(f . y)) = 0 by METRIC_1:1;
dist (z,y) >= 0 by METRIC_1:5;
hence dist ((f . z),(f . y)) <= (1 / 2) * (dist (z,y)) by A1; :: thesis: verum