let G be RelStr ; :: thesis: 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; :: thesis: 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) ; :: thesis: verum

let H be full SubRelStr of G; :: thesis: 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) ; :: thesis: verum