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 :: 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 ) implies S embeds R )
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 object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: 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 2;
then [x2,x2] in the InternalRel of R by A3;
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 5;
[x1,x1] in the InternalRel of R by A3, A6;
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 5;
hence x1 = x2 by ; :: thesis: verum
end;
then f is one-to-one by FUNCT_1:def 4;
hence S embeds R by A2; :: thesis: verum
end;
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 A1; :: thesis: verum