:: deftheorem defines VertexAdjSymRel GLUNIR00:def 2 :
for G being _Graph holds VertexAdjSymRel G = (VertexDomRel G) \/ ((VertexDomRel G) ~);