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

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 )

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

then reconsider f = id the carrier of H as Function of the carrier of H, the carrier of G by A1, FUNCT_2:3;
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;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

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

hence
G embeds H
; :: thesis: verum
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 )

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;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
[(f . x),(f . y)] in the InternalRel of G
; :: thesis: [x,y] in the InternalRel of H
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;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

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