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 A2: 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 A2; :: thesis: verum