let x, y, z be set ; :: thesis: ( x is_a_fixpoint_of {[y,z]} implies x = y )
assume A1: x in dom {[y,z]} ; :: according to ABIAN:def 3 :: thesis: ( not x = {[y,z]} . x or x = y )
dom {[y,z]} = {y} by RELAT_1:9;
hence ( not x = {[y,z]} . x or x = y ) by A1, TARSKI:def 1; :: thesis: verum