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 )

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

( 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 )

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 ) 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

hence S embeds R by A2; :: thesis: verum

end;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

then
f is one-to-one
by FUNCT_1:def 4;
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 A7, ORDERS_2:2; :: thesis: verum

end;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 A7, ORDERS_2:2; :: thesis: verum

hence S embeds R by A2; :: thesis: verum

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