let X be trivial set ; :: thesis: for x being set st x in X holds

for f being Function of X,X holds x is_a_fixpoint_of f

let x be set ; :: thesis: ( x in X implies for f being Function of X,X holds x is_a_fixpoint_of f )

assume A1: x in X ; :: thesis: for f being Function of X,X holds x is_a_fixpoint_of f

then consider y being object such that

A2: X = {y} by ZFMISC_1:131;

let f be Function of X,X; :: thesis: x is_a_fixpoint_of f

thus x in dom f by A1, FUNCT_2:52; :: according to ABIAN:def 3 :: thesis: x = f . x

then A3: f . x in rng f by FUNCT_1:def 3;

A4: rng f c= X by RELAT_1:def 19;

thus x = y by A1, A2, TARSKI:def 1

.= f . x by A2, A3, A4, TARSKI:def 1 ; :: thesis: verum

for f being Function of X,X holds x is_a_fixpoint_of f

let x be set ; :: thesis: ( x in X implies for f being Function of X,X holds x is_a_fixpoint_of f )

assume A1: x in X ; :: thesis: for f being Function of X,X holds x is_a_fixpoint_of f

then consider y being object such that

A2: X = {y} by ZFMISC_1:131;

let f be Function of X,X; :: thesis: x is_a_fixpoint_of f

thus x in dom f by A1, FUNCT_2:52; :: according to ABIAN:def 3 :: thesis: x = f . x

then A3: f . x in rng f by FUNCT_1:def 3;

A4: rng f c= X by RELAT_1:def 19;

thus x = y by A1, A2, TARSKI:def 1

.= f . x by A2, A3, A4, TARSKI:def 1 ; :: thesis: verum