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 set such that
A2: X = {y} by REALSET1:def 4;
let f be Function of X,X; :: thesis: x is_a_fixpoint_of f
thus x in dom f by A1, FUNCT_2:67; :: according to ABIAN:def 3 :: thesis: x = f . x
then A3: f . x in rng f by FUNCT_1:def 5;
A4: rng f c= X by RELSET_1:12;
thus x = y by A1, A2, TARSKI:def 1
.= f . x by A2, A3, A4, TARSKI:def 1 ; :: thesis: verum