thus omega is regular by CARD_5:42; :: according to CARD_FIL:def 13 :: thesis: omega is limit_cardinal
thus omega is limit_cardinal ; :: thesis: verum