theorem Th2: :: ORDINAL7:2

for a being Ordinal holds a +^ a = 2 *^ a