for A being Ordinal st A is_cofinal_with {} holds
A = {} by ORDINAL2:50;