let a, b, c be Ordinal; :: 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);
A1: for n being Nat holds
( n in omega & omega in Tarski-Class ((c \/ b) \/ omega) & omega in Tarski-Class ((c \/ a) \/ omega) ) by Th57, ORDINAL1:def 12;
A2: ( b in Tarski-Class ((c \/ b) \/ omega) & c in Tarski-Class ((c \/ b) \/ omega) ) by Th66;
A3: ( a in Tarski-Class ((c \/ a) \/ omega) & c in Tarski-Class ((c \/ a) \/ omega) ) by Th66;
reconsider f = ((Tarski-Class ((c \/ b) \/ omega)) -Veblen) . c as increasing Ordinal-Sequence of (Tarski-Class ((c \/ b) \/ omega)) by A1, Th66, Th62;
reconsider g = ((Tarski-Class ((c \/ a) \/ omega)) -Veblen) . c as increasing Ordinal-Sequence of (Tarski-Class ((c \/ a) \/ omega)) by A1, Th66, Th62;
A4: ( dom f = On (Tarski-Class ((c \/ b) \/ omega)) & dom g = On (Tarski-Class ((c \/ a) \/ omega)) ) by FUNCT_2:def 1;
A5: ( b in On (Tarski-Class ((c \/ b) \/ omega)) & a in On (Tarski-Class ((c \/ a) \/ omega)) ) by A2, A3, ORDINAL1:def 9;

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

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

per cases ( a = b or a c< b ) by A6;

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 A4, A5, ORDINAL2:def 12;
then c -Veblen a in c -Veblen b by A7, A1, A2, A3, Th64;
hence c -Veblen a c= c -Veblen b by ORDINAL1:def 2; :: thesis: verum

end;

end;

end;

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