theorem Th2: :: ORDEQ_01:2
for x, y, z being set st x is_a_fixpoint_of {[y,z]} holds
x = y