theorem Th71: :: ORDINAL6:71
for a, b, c being Ordinal holds
( a c= b iff c -Veblen a c= c -Veblen b )