assume id {} has_a_fixpoint ; :: thesis: contradiction
then consider y being set such that
A1: y is_a_fixpoint_of id {} by ABIAN:def 5;
y in dom (id {}) by A1, ABIAN:def 3;
hence contradiction ; :: thesis: verum