for A being Ordinal st A is_cofinal_with 0 holds
A = 0