n c= omega ;
then n \/ omega = omega by XBOOLE_1:12;
hence for b₁ being Ordinal holds
( b₁ = n -Veblen b iff b₁ = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b ) by XBOOLE_1:4; :: thesis: verum