set I = id X;
set x = the Element of X;
the Element of X in fixpoints (id X) ;
hence id X is with_fixpoint by ABIAN:def 5, Lm78; :: thesis: verum