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

assume X =^ Y ; :: thesis: ( X c=^ Y & Y c=^ X )
then UAp X = UAp Y by Def15;
hence ( X c=^ Y & Y c=^ X ) by Def12; :: thesis: verum

end;

assume ( X c=^ Y & Y c=^ X ) ; :: thesis: X =^ Y
then ( UAp X c= UAp Y & UAp Y c= UAp X ) by Def12;
then UAp X = UAp Y by XBOOLE_0:def 10;
hence X =^ Y by Def15; :: thesis: verum