let R, S, T be non empty RelStr ; :: thesis: ( R is_equimorphic_to S & S is_equimorphic_to T implies R is_equimorphic_to T )
assume A1: ( R is_equimorphic_to S & S is_equimorphic_to T ) ; :: thesis: R is_equimorphic_to T
then ( S embeds R & T embeds S ) by Def3;
then A2: T embeds R by Th13;
( R embeds S & S embeds T ) by A1, Def3;
then R embeds T by Th13;
hence R is_equimorphic_to T by A2, Def3; :: thesis: verum