theorem Th69: :: ORDINAL6:69

for a, b being Ordinal holds b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a