let X, Y, Z be set ; :: thesis: ( X c= Y & Y c= Z & X,Z are_equipotent implies ( X,Y are_equipotent & Y,Z are_equipotent ) )
assume that
A1: ( X c= Y & Y c= Z ) and
A2: X,Z are_equipotent ; :: thesis: ( X,Y are_equipotent & Y,Z are_equipotent )
A3: card X = card Z by A2, Th21;
( card X c= card Y & card Y c= card Z ) by A1, Th27;
then card X = card Y by A3, XBOOLE_0:def 10;
hence ( X,Y are_equipotent & Y,Z are_equipotent ) by A3, Th21; :: thesis: verum