let R be reflexive antisymmetric RelStr ; :: thesis: for S being RelStr holds
( ex f being Function of R,S st
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 ) iff S embeds R )
let S be RelStr ; :: thesis: ( ex f being Function of R,S st
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 ) iff S embeds R )

A1: now

assume ex f being Function of R,S st
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 ) ; :: thesis: S embeds R
then consider f being Function of R,S such that
A2: 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 ) ;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of R by A3, A4;
A6: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 4;
then [x2,x2] in the InternalRel of R by A3, RELAT_2:def 1;
then [(f . x2),(f . x1)] in the InternalRel of S by A2, A5;
then [x2,x1] in the InternalRel of R by A2;
then A7: x2 <= x1 by ORDERS_2:def 9;
[x1,x1] in the InternalRel of R by A3, A6, RELAT_2:def 1;
then [(f . x1),(f . x2)] in the InternalRel of S by A2, A5;
then [x1,x2] in the InternalRel of R by A2;
then x1 <= x2 by ORDERS_2:def 9;
hence x1 = x2 by A7, ORDERS_2:25; :: thesis: verum

end;

then f is one-to-one by FUNCT_1:def 8;
hence S embeds R by A2, NECKLACE:def 2; :: thesis: verum

end;

now

assume A8: S embeds R ; :: thesis: ex f being Function of R,S st
( ex f being Function of R,S st
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 ) iff S embeds R )
then consider f being Function of R,S such that
f is one-to-one and
A9: 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 ) by NECKLACE:def 2;
take f = f; :: thesis: ( ex f being Function of R,S st
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 ) iff S embeds R )
thus ( ex f being Function of R,S st
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 ) iff S embeds R ) by A8, A9; :: thesis: verum

end;

hence ( ex f being Function of R,S st
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 ) iff S embeds R ) by A1; :: thesis: verum