set f = {[x,x]};
A1: dom {[x,x]} = {x} by RELAT_1:9;
take x ; :: according to ORDEQ_01:def 1 :: thesis: ( x is_a_fixpoint_of {[x,x]} & ( for y being set st y is_a_fixpoint_of {[x,x]} holds
x = y ) )
thus x is_a_fixpoint_of {[x,x]} :: thesis: for y being set st y is_a_fixpoint_of {[x,x]} holds
x = y

proof

thus A2: x in dom {[x,x]} by A1, TARSKI:def 1; :: according to ABIAN:def 3 :: thesis: x = {[x,x]} . x
[x,x] in {[x,x]} by TARSKI:def 1;
hence x = {[x,x]} . x by A2, FUNCT_1:def 2; :: thesis: verum

end;

let b be set ; :: thesis: ( b is_a_fixpoint_of {[x,x]} implies x = b )
assume b is_a_fixpoint_of {[x,x]} ; :: thesis: x = b
then b = x by Th2;
hence x = b ; :: thesis: verum