thus card omega = omega by CARD_1:84; :: according to CARD_3:def 16 :: thesis: verum