thus card omega = omega by CARD_1:47; :: according to CARD_3:def 15 :: thesis: verum