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

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

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

thus
( [(h . x),(h . y)] in the InternalRel of R implies [x,y] in the InternalRel of T )
:: thesis: verum
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;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