let a, b, c be Ordinal; :: thesis: ( a in b iff c -Veblen a in c -Veblen b )
( b c= a iff c -Veblen b c= c -Veblen a ) by Th71;
hence ( a in b iff c -Veblen a in c -Veblen b ) by Th4; :: thesis: verum