for M being non empty MetrSpace
for f being Contraction of M st M is complete holds
ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )