hereby :: thesis: ( X _c= Y & Y _c= X implies X _= Y )

assume X _= Y ; :: thesis: ( X _c= Y & Y _c= X )
then LAp X = LAp Y by Def14;
hence ( X _c= Y & Y _c= X ) by Def11; :: thesis: verum

end;

assume ( X _c= Y & Y _c= X ) ; :: thesis: X _= Y
then ( LAp X c= LAp Y & LAp Y c= LAp X ) by Def11;
then LAp X = LAp Y by XBOOLE_0:def 10;
hence X _= Y by Def14; :: thesis: verum