theorem :: ORDINAL3:62

for A, B being Ordinal holds A c= B +^ (A -^ B)