:: deftheorem defines is_a_fixpoint_of ABIAN:def 4 :
for A being non empty set
for a being Element of A
for f being Function of A,A holds
( a is_a_fixpoint_of f iff a = f . a );