theorem Th16: :: ORDINAL5:16

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