let G2 be _Graph; :: thesis: for G1 being reverseEdgeDirections of G2 holds
( the_Source_of G1 = the_Target_of G2 & the_Target_of G1 = the_Source_of G2 )
let G1 be reverseEdgeDirections of G2; :: thesis: ( the_Source_of G1 = the_Target_of G2 & the_Target_of G1 = the_Source_of G2 )
A1: ( dom (the_Target_of G2) = the_Edges_of G2 & dom (the_Source_of G2) = the_Edges_of G2 ) by FUNCT_2:def 1;
thus the_Source_of G1 = (the_Source_of G2) +* ((the_Target_of G2) | (the_Edges_of G2)) by Def1
.= the_Target_of G2 by A1, FUNCT_4:19 ; :: thesis: the_Target_of G1 = the_Source_of G2
thus the_Target_of G1 = (the_Target_of G2) +* ((the_Source_of G2) | (the_Edges_of G2)) by Def1
.= the_Source_of G2 by A1, FUNCT_4:19 ; :: thesis: verum