assume id {} is with_fixpoint ; :: thesis: contradiction
then consider y being object 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