:: deftheorem defines is_equimorphic_to NECKLACE:def 2 :
for R, S being non empty RelStr holds
( R is_equimorphic_to S iff ( R embeds S & S embeds R ) );