let G2 be _Graph; for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E holds
( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 )
let E be set ; for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E holds
( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 )
let G1 be reverseEdgeDirections of G2,E; for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E holds
( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 )
let v1, e, v2 be object ; ( E c= the_Edges_of G2 & not e in E implies ( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 ) )
assume A1:
( E c= the_Edges_of G2 & not e in E )
; ( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 )
hence
( e DJoins v1,v2,G2 implies e DJoins v1,v2,G1 )
by Lm2; ( e DJoins v1,v2,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 v1,v2,G1 implies e DJoins v1,v2,G3 )
by A1, Lm2;
hence
( e DJoins v1,v2,G1 implies e DJoins v1,v2,G2 )
; verum