let G be non empty RelStr ; :: thesis: for H being non empty full SubRelStr of G holds G embeds H
let H be non empty full SubRelStr of G; :: thesis: G embeds H
reconsider f = id the carrier of H as Function of the carrier of H,the carrier of H ;
A1: the carrier of H c= the carrier of G by YELLOW_0:def 13;
A2: dom f = the carrier of H by FUNCT_1:34;
for x being set st x in the carrier of H holds
f . x in the carrier of G

proof

let x be set ; :: thesis: ( x in the carrier of H implies f . x in the carrier of G )
assume x in the carrier of H ; :: thesis: f . x in the carrier of G
then f . x in the carrier of H by FUNCT_1:34;
hence f . x in the carrier of G by A1; :: thesis: verum

end;

then reconsider f = id the carrier of H as Function of the carrier of H,the carrier of G by A2, FUNCT_2:5;
reconsider f = f as Function of H,G ;
for x, y being Element of H holds
( [x,y] in the InternalRel of H iff [(f . x),(f . y)] in the InternalRel of G )

proof

let x, y be Element of H; :: thesis: ( [x,y] in the InternalRel of H iff [(f . x),(f . y)] in the InternalRel of G )
set IH = the InternalRel of H;
set IG = the InternalRel of G;
set cH = the carrier of H;
A3: ( f . x = x & f . y = y ) by FUNCT_1:34;
thus ( [x,y] in the InternalRel of H implies [(f . x),(f . y)] in the InternalRel of G ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of G implies [x,y] in the InternalRel of H )

proof

assume [x,y] in the InternalRel of H ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then [x,y] in the InternalRel of G |_2 the carrier of H by YELLOW_0:def 14;
hence [(f . x),(f . y)] in the InternalRel of G by A3, XBOOLE_0:def 4; :: thesis: verum

end;

assume [(f . x),(f . y)] in the InternalRel of G ; :: thesis: [x,y] in the InternalRel of H
then [x,y] in the InternalRel of G |_2 the carrier of H by A3, XBOOLE_0:def 4;
hence [x,y] in the InternalRel of H by YELLOW_0:def 14; :: thesis: verum

end;

hence G embeds H by NECKLACE:def 2; :: thesis: verum