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 Def2;
then A2: T embeds R by Th12;
( R embeds S & S embeds T ) by A1, Def2;
then R embeds T by Th12;
hence R is_equimorphic_to T by A2, Def2; :: thesis: verum