:: deftheorem defines with_fixpoint ABIAN:def 5 :
for f being Function holds
( f is with_fixpoint iff ex x being object st x is_a_fixpoint_of f );