let R be non empty RelStr ; :: thesis: R embeds R
set f = id the carrier of R;
reconsider f = id the carrier of R as Function of R,R ;
take f ; :: according to NECKLACE:def 2 :: thesis: ( 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 R ) ) )
thus f is one-to-one ; :: thesis: for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R )
let x, y be Element of R; :: thesis: ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R )
( x = f . x & y = f . y ) by FUNCT_1:35;
hence ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) ; :: thesis: verum