let R be reflexive antisymmetric RelStr ; 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 ; ( 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 ( 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 )
;
S embeds Rthen 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 ;
( 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
;
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;
verum
end; then
f is
one-to-one
by FUNCT_1:def 4;
hence
S embeds R
by A2;
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; verum