thus ( X _= Y implies ( X _c= Y & Y _c= X ) ) ; :: thesis: ( X _c= Y & Y _c= X implies X _= Y )
assume ( X _c= Y & Y _c= X ) ; :: thesis: X _= Y
then ( LAp X c= LAp Y & LAp Y c= LAp X ) ;
then LAp X = LAp Y ;
hence X _= Y ; :: thesis: verum