theorem Th60: :: ORDINAL6:60
for a, b, c being Ordinal
for U being Universe st a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) & ( for c being Ordinal st c in b holds
(U -Veblen) . c is normal ) holds
((U -Veblen) . a) . c c= ((U -Veblen) . b) . c