theorem Th21: :: CARD_5:22

cf omega = omega