let R be non empty RelStr ; :: thesis: (R,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 1 :: 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 )
thus ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) ; :: thesis: verum