theorem Th3: :: HILBERT3:3

for X being trivial set
for x being set st x in X holds
for f being Function of X,X holds x is_a_fixpoint_of f