let a, b, c be ordinal number ; :: thesis: ( a c= b iff c -Veblen a c= c -Veblen b )
set U = Tarski-Class ((c \/ b) \/ omega);
set W = Tarski-Class ((c \/ a) \/ omega);
A0: for n being Nat holds
( n in omega & omega in Tarski-Class ((c \/ b) \/ omega) & omega in Tarski-Class ((c \/ a) \/ omega) ) by Unc1, ORDINAL1:def 12;
A1: ( b in Tarski-Class ((c \/ b) \/ omega) & c in Tarski-Class ((c \/ b) \/ omega) ) by LemT;
A2: ( a in Tarski-Class ((c \/ a) \/ omega) & c in Tarski-Class ((c \/ a) \/ omega) ) by LemT;
reconsider f = ((Tarski-Class ((c \/ b) \/ omega)) -Veblen) . c as increasing Ordinal-Sequence of (Tarski-Class ((c \/ b) \/ omega)) by A0, LemT, Th23;
reconsider g = ((Tarski-Class ((c \/ a) \/ omega)) -Veblen) . c as increasing Ordinal-Sequence of (Tarski-Class ((c \/ a) \/ omega)) by A0, LemT, Th23;
A3: ( dom f = On (Tarski-Class ((c \/ b) \/ omega)) & dom g = On (Tarski-Class ((c \/ a) \/ omega)) ) by FUNCT_2:def 1;
A4: ( b in On (Tarski-Class ((c \/ b) \/ omega)) & a in On (Tarski-Class ((c \/ a) \/ omega)) ) by A1, A2, ORDINAL1:def 9;

hereby :: thesis: ( c -Veblen a c= c -Veblen b implies a c= b )

assume B1: a c= b ; :: thesis: c -Veblen a c= c -Veblen b
then B2: a in Tarski-Class ((c \/ b) \/ omega) by A1, CLASSES1:def 1;

per cases ( a = b or a c< b ) by B1, XBOOLE_0:def 8;

suppose a = b ; :: thesis: c -Veblen a c= c -Veblen b

hence c -Veblen a c= c -Veblen b ; :: thesis: verum

end;

suppose a c< b ; :: thesis: c -Veblen a c= c -Veblen b

then a in b by ORDINAL1:11;
then f . a in f . b by A3, A4, ORDINAL2:def 12;
then c -Veblen a in c -Veblen b by B2, A0, A1, A2, Th25;
hence c -Veblen a c= c -Veblen b by ORDINAL1:def 2; :: thesis: verum

end;

end;

end;

assume A5: ( c -Veblen a c= c -Veblen b & a c/= b ) ; :: thesis: contradiction
then A6: b in a by ORDINAL1:16;
then A7: b in Tarski-Class ((c \/ a) \/ omega) by A2, ORDINAL1:10;
g . b in g . a by A3, A4, A6, ORDINAL2:def 12;
then c -Veblen b in c -Veblen a by A0, A1, A2, A7, Th25;
then c -Veblen b in c -Veblen b by A5;
hence contradiction ; :: thesis: verum