theorem Th27: :: ORDINAL3:27

for A, B being Ordinal st A c= B holds
ex C being Ordinal st B = A +^ C