:: deftheorem defines embeds NECKLACE:def 1 :
for R, S being RelStr holds
( S embeds R iff ex f being Function of R,S st
( f is one-to-one & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) ) ) );