let R, S, T be non empty RelStr ; :: thesis: ( R embeds S & S embeds T implies R embeds T )
assume R embeds S ; :: thesis: ( not S embeds T or R embeds T )
then consider f being Function of S,R such that
A1: f is one-to-one and
A2: for x, y being Element of S holds
( [x,y] in the InternalRel of S iff [(f . x),(f . y)] in the InternalRel of R ) ;
assume S embeds T ; :: thesis: R embeds T
then consider g being Function of T,S such that
A3: g is one-to-one and
A4: for x, y being Element of T holds
( [x,y] in the InternalRel of T iff [(g . x),(g . y)] in the InternalRel of S ) ;
reconsider h = f * g as Function of T,R ;
take h ; :: according to NECKLACE:def 1 :: thesis: ( h is one-to-one & ( for x, y being Element of T holds
( [x,y] in the InternalRel of T iff [(h . x),(h . y)] in the InternalRel of R ) ) )
thus h is one-to-one by A1, A3; :: thesis: for x, y being Element of T holds
( [x,y] in the InternalRel of T iff [(h . x),(h . y)] in the InternalRel of R )
thus for x, y being Element of T holds
( [x,y] in the InternalRel of T iff [(h . x),(h . y)] in the InternalRel of R ) :: thesis: verum

proof

let x, y be Element of T; :: thesis: ( [x,y] in the InternalRel of T iff [(h . x),(h . y)] in the InternalRel of R )
thus ( [x,y] in the InternalRel of T implies [(h . x),(h . y)] in the InternalRel of R ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of R implies [x,y] in the InternalRel of T )

proof

assume [x,y] in the InternalRel of T ; :: thesis: [(h . x),(h . y)] in the InternalRel of R
then A5: [(g . x),(g . y)] in the InternalRel of S by A4;
( h . x = f . (g . x) & h . y = f . (g . y) ) by FUNCT_2:15;
hence [(h . x),(h . y)] in the InternalRel of R by A2, A5; :: thesis: verum

end;

thus ( [(h . x),(h . y)] in the InternalRel of R implies [x,y] in the InternalRel of T ) :: thesis: verum

proof

A6: ( h . x = f . (g . x) & h . y = f . (g . y) ) by FUNCT_2:15;
assume [(h . x),(h . y)] in the InternalRel of R ; :: thesis: [x,y] in the InternalRel of T
then [(g . x),(g . y)] in the InternalRel of S by A2, A6;
hence [x,y] in the InternalRel of T by A4; :: thesis: verum

end;

end;