theorem Th1: :: CARDFIN2:1

id {} is without_fixpoints