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

assume X _=^ Y ; :: thesis: ( X _= Y & X =^ Y )
then ( LAp X = LAp Y & UAp X = UAp Y ) by Def16;
hence ( X _= Y & X =^ Y ) by Def14, Def15; :: thesis: verum

end;

assume ( X _= Y & X =^ Y ) ; :: thesis: X _=^ Y
then ( LAp X = LAp Y & UAp X = UAp Y ) by Def14, Def15;
hence X _=^ Y by Def16; :: thesis: verum