let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies VertexAdjSymRel G1 = VertexAdjSymRel G2 )
assume A1: G1 == G2 ; :: thesis: VertexAdjSymRel G1 = VertexAdjSymRel G2
thus VertexAdjSymRel G1 = (VertexDomRel G2) \/ ((VertexDomRel G1) ~) by A1, Th19
.= VertexAdjSymRel G2 by A1, Th19 ; :: thesis: verum