theorem :: ORDINAL2:3

for A being Ordinal holds succ A c= bool A