theorem Th6: :: CARD_4:6

omega *` omega = omega by Th5, CARD_2:def 2;