theorem Th27: :: ORDINAL6:27

for x being set
for f being Function st x is_a_fixpoint_of f holds
x in rng f by FUNCT_1:def 3;