let G be RelStr ; for H being full SubRelStr of G holds the InternalRel of (ComplRelStr H) = the InternalRel of (ComplRelStr G) |_2 the carrier of (ComplRelStr H)
let H be full SubRelStr of G; the InternalRel of (ComplRelStr H) = the InternalRel of (ComplRelStr G) |_2 the carrier of (ComplRelStr H)
set IH = the InternalRel of H;
set ICmpH = the InternalRel of (ComplRelStr H);
set cH = the carrier of H;
set IG = the InternalRel of G;
set cG = the carrier of G;
set ICmpG = the InternalRel of (ComplRelStr G);
A1: the InternalRel of (ComplRelStr H) =
( the InternalRel of H `) \ (id the carrier of H)
by NECKLACE:def 8
.=
([: the carrier of H, the carrier of H:] \ the InternalRel of H) \ (id the carrier of H)
by SUBSET_1:def 4
;
A2: the InternalRel of (ComplRelStr G) =
( the InternalRel of G `) \ (id the carrier of G)
by NECKLACE:def 8
.=
([: the carrier of G, the carrier of G:] \ the InternalRel of G) \ (id the carrier of G)
by SUBSET_1:def 4
;
A3:
the carrier of H c= the carrier of G
by YELLOW_0:def 13;
the InternalRel of (ComplRelStr G) |_2 the carrier of (ComplRelStr H) =
the InternalRel of (ComplRelStr G) |_2 the carrier of H
by NECKLACE:def 8
.=
(([: the carrier of G, the carrier of G:] \ the InternalRel of G) /\ [: the carrier of H, the carrier of H:]) \ ((id the carrier of G) /\ [: the carrier of H, the carrier of H:])
by A2, XBOOLE_1:50
.=
(([: the carrier of G, the carrier of G:] /\ [: the carrier of H, the carrier of H:]) \ ( the InternalRel of G /\ [: the carrier of H, the carrier of H:])) \ ((id the carrier of G) /\ [: the carrier of H, the carrier of H:])
by XBOOLE_1:50
.=
(([: the carrier of G, the carrier of G:] /\ [: the carrier of H, the carrier of H:]) \ ( the InternalRel of G /\ [: the carrier of H, the carrier of H:])) \ ((id the carrier of G) | the carrier of H)
by Th1
.=
(([: the carrier of G, the carrier of G:] /\ [: the carrier of H, the carrier of H:]) \ ( the InternalRel of G |_2 the carrier of H)) \ (id the carrier of H)
by A3, FUNCT_3:1
.=
(([: the carrier of G, the carrier of G:] /\ [: the carrier of H, the carrier of H:]) \ the InternalRel of H) \ (id the carrier of H)
by YELLOW_0:def 14
.=
([:( the carrier of G /\ the carrier of H),( the carrier of G /\ the carrier of H):] \ the InternalRel of H) \ (id the carrier of H)
by ZFMISC_1:100
.=
([: the carrier of H,( the carrier of G /\ the carrier of H):] \ the InternalRel of H) \ (id the carrier of H)
by A3, XBOOLE_1:28
.=
the InternalRel of (ComplRelStr H)
by A1, A3, XBOOLE_1:28
;
hence
the InternalRel of (ComplRelStr H) = the InternalRel of (ComplRelStr G) |_2 the carrier of (ComplRelStr H)
; verum