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