let G be RelStr ; :: thesis: for H being full SubRelStr of G holds the InternalRel of () = the InternalRel of () |_2 the carrier of ()
let H be full SubRelStr of G; :: thesis: the InternalRel of () = the InternalRel of () |_2 the carrier of ()
set IH = the InternalRel of H;
set ICmpH = the InternalRel of ();
set cH = the carrier of H;
set IG = the InternalRel of G;
set cG = the carrier of G;
set ICmpG = the InternalRel of ();
A1: the InternalRel of () = ( 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 () = ( 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 () |_2 the carrier of () = the InternalRel of () |_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
.= (([: 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
.= (([: 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
.= the InternalRel of () by ;
hence the InternalRel of () = the InternalRel of () |_2 the carrier of () ; :: thesis: verum