theorem Th17: :: ORDINAL5:17

for a being Ordinal holds 1 |^|^ a = 1