let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )
let G1 be reverseEdgeDirections of G2,E; :: thesis: for v1, e, v2 being object st E c= the_Edges_of G2 & e in E holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )
let v1, e, v2 be object ; :: thesis: ( E c= the_Edges_of G2 & e in E implies ( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 ) )
assume A1: ( E c= the_Edges_of G2 & e in E ) ; :: thesis: ( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )
hence ( e DJoins v1,v2,G2 implies e DJoins v2,v1,G1 ) by Lm1; :: thesis: ( e DJoins v2,v1,G1 implies e DJoins v1,v2,G2 )
reconsider G3 = G2 as reverseEdgeDirections of G1,E by Th3;
E c= the_Edges_of G1 by Th4, A1;
then ( e DJoins v2,v1,G1 implies e DJoins v1,v2,G3 ) by A1, Lm1;
hence ( e DJoins v2,v1,G1 implies e DJoins v1,v2,G2 ) ; :: thesis: verum