let a, b be Ordinal; :: thesis: ( a in b iff epsilon_ a in epsilon_ b )
( b c/= a iff epsilon_ b c/= epsilon_ a ) by Th11;
hence ( a in b iff epsilon_ a in epsilon_ b ) by Th4; :: thesis: verum