consider x being object such that
A1: x is_a_fixpoint_of f by ABIAN:def 5;
thus not fixpoints f is empty by A1, Lm78; :: thesis: verum