theorem :: GLUNIR00:35

for G being _Graph holds VertexAdjSymRel G = (((the_Source_of G) ~) * (the_Target_of G)) \/ (((the_Target_of G) ~) * (the_Source_of G))