let a, b be Ordinal; :: thesis: ( a c= b iff epsilon_ a c= epsilon_ b )

hereby :: thesis: ( epsilon_ a c= epsilon_ b implies a c= b )

assume a c= b ; :: thesis: epsilon_ a c= epsilon_ b
then ( a = b or a c< b ) ;
then ( a = b or epsilon_ a in epsilon_ b ) by ORDINAL1:11, ORDINAL5:44;
hence epsilon_ a c= epsilon_ b by ORDINAL1:def 2; :: thesis: verum

end;

assume A1: epsilon_ a c= epsilon_ b ; :: thesis: a c= b
assume a c/= b ; :: thesis: contradiction
then epsilon_ b in epsilon_ a by ORDINAL1:16, ORDINAL5:44;
then epsilon_ b in epsilon_ b by A1;
hence contradiction ; :: thesis: verum