let G be _Graph; :: thesis: for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) /\ [:V,V:]
let V be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) /\ [:V,V:]
let H be inducedSubgraph of G,V; :: thesis: VertexAdjSymRel H = (VertexAdjSymRel G) /\ [:V,V:]
A1: VertexDomRel H = (VertexDomRel G) /\ [:V,V:] by Th21;
then (VertexDomRel H) ~ = ((VertexDomRel G) ~) /\ ([:V,V:] ~) by RELAT_1:22
.= ((VertexDomRel G) ~) /\ [:V,V:] by SYSREL:5 ;
hence VertexAdjSymRel H = (VertexAdjSymRel G) /\ [:V,V:] by A1, XBOOLE_1:23; :: thesis: verum