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 ( UAp X c= UAp Y & UAp Y c= UAp X ) ;
then UAp X = UAp Y ;
hence X =^ Y ; :: thesis: verum