let a, b, c be ordinal number ; :: thesis: ( a in b iff c -Veblen a in c -Veblen b )
( b c= a iff c -Veblen b c= c -Veblen a ) by Th15;
hence ( a in b iff c -Veblen a in c -Veblen b ) by EXCH1; :: thesis: verum