:: deftheorem defines -Veblen ORDINAL6:def 16 :
for a, b being Ordinal holds a -Veblen b = (((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b;