theorem Th64: :: ORDINAL3:64

for A, B being Ordinal holds (A div^ B) *^ B c= A