let a, b be ordinal number ; :: thesis: ( a in b iff epsilon_ a in epsilon_ b )
( b c/= a iff epsilon_ b c/= epsilon_ a ) by LemE1;
hence ( a in b iff epsilon_ a in epsilon_ b ) by EXCH1; :: thesis: verum