let G be _Graph; :: thesis: VertexAdjSymRel G = (((the_Source_of G) ~) * (the_Target_of G)) \/ (((the_Target_of G) ~) * (the_Source_of G))
set S = the_Source_of G;
set T = the_Target_of G;
thus VertexAdjSymRel G = (((the_Source_of G) ~) * (the_Target_of G)) \/ (((the_Target_of G) ~) * (((the_Source_of G) ~) ~)) by RELAT_1:35
.= (((the_Source_of G) ~) * (the_Target_of G)) \/ (((the_Target_of G) ~) * (the_Source_of G)) ; :: thesis: verum