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 9
.=
([:the carrier of H,the carrier of H:] \ the InternalRel of H) \ (id the carrier of H)
by SUBSET_1:def 5
;
A2: the InternalRel of (ComplRelStr G) =
(the InternalRel of G ` ) \ (id the carrier of G)
by NECKLACE:def 9
.=
([:the carrier of G,the carrier of G:] \ the InternalRel of G) \ (id the carrier of G)
by SUBSET_1:def 5
;
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 9
.=
(([: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:123
.=
([: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