begin
:: deftheorem Def1 defines contraction ALI2:def 1 :
for M being non empty MetrSpace
for b2 being Function of M,M holds
( b2 is contraction of M iff ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds dist (b2 . x),(b2 . y) <= L * (dist x,y) ) ) );
theorem
canceled;
theorem