let M, N be Cardinal; :: thesis: ( X,M are_equipotent & X,N are_equipotent implies M = N )
assume ( X,M are_equipotent & X,N are_equipotent ) ; :: thesis: M = N
then M,N are_equipotent by WELLORD2:15;
hence M = N by Th8; :: thesis: verum