theorem :: ORDEQ_01:1

for x being set holds x is_a_fixpoint_of {[x,x]}