(VertexAdjSymRel G) ~ = ((VertexDomRel G) ~) \/ (((VertexDomRel G) ~) ~) by RELAT_1:23
.= VertexAdjSymRel G ;
hence VertexAdjSymRel G is symmetric by RELAT_2:13; :: thesis: verum