:: deftheorem defines -Veblen ORDINAL6:def 17 :
for n being Nat
for b being Ordinal holds n -Veblen b = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b;