for X being trivial set
for x being set st x in X holds
for f being Function of X,X holds x is_a_fixpoint_of f