theorem Th13: :: KNASTER:13

for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (f,0) +. x = x