let X, Y, Z be set ; ( 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
; ( X,Y are_equipotent & Y,Z are_equipotent )
A3:
card X = card Z
by A2, Th4;
( card X c= card Y & card Y c= card Z )
by A1, Th10;
hence
( X,Y are_equipotent & Y,Z are_equipotent )
by A3, Th4, XBOOLE_0:def 10; verum