theorem :: ORDINAL2:50

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