let x be set ; :: thesis: x is_a_fixpoint_of {[x,x]}
A1: [x,x] in {[x,x]} by TARSKI:def 1;
dom {[x,x]} = {x} by RELAT_1:9;
hence x in dom {[x,x]} by TARSKI:def 1; :: according to ABIAN:def 3 :: thesis: x = {[x,x]} . x
hence x = {[x,x]} . x by A1, FUNCT_1:def 2; :: thesis: verum