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: dom f = the carrier of H ;
A2: the carrier of H c= the carrier of G by YELLOW_0:def 13;
for x being object st x in the carrier of H holds
f . x in the carrier of G
proof
let x be object ; :: 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:17;
hence f . x in the carrier of G by A2; :: thesis: verum
end;
then reconsider f = id the carrier of H as Function of the carrier of H, the carrier of G by A1, FUNCT_2:3;
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
set IH = the InternalRel of H;
set IG = the InternalRel of G;
set cH = the carrier of H;
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 )
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 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 XBOOLE_0:def 4;
hence [x,y] in the InternalRel of H by YELLOW_0:def 14; :: thesis: verum
end;
hence G embeds H ; :: thesis: verum