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 ( R is_equimorphic_to S & S is_equimorphic_to T ) ; :: thesis: R is_equimorphic_to T
then ( R embeds S & S embeds R & S embeds T & T embeds S ) by Def3;
then ( R embeds T & T embeds R ) by Th13;
hence R is_equimorphic_to T by Def3; :: thesis: verum