let G be _Graph; :: thesis: for H being Subgraph of G holds VertexAdjSymRel H c= VertexAdjSymRel G
let H be Subgraph of G; :: thesis: VertexAdjSymRel H c= VertexAdjSymRel G
A1: VertexDomRel H c= VertexDomRel G by Th15;
then (VertexDomRel H) ~ c= (VertexDomRel G) ~ by SYSREL:11;
hence VertexAdjSymRel H c= VertexAdjSymRel G by A1, XBOOLE_1:13; :: thesis: verum