theorem :: FOMODEL0:69

for x being set
for f being Function holds
( x in fixpoints f iff x is_a_fixpoint_of f ) by Lm78;