let G1 be reverseEdgeDirections of G,E; :: thesis: G1 is connected
for v1, v2 being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from v1,v2

proof

let v1, v2 be Vertex of G1; :: thesis: ex W1 being Walk of G1 st W1 is_Walk_from v1,v2
reconsider w1 = v1, w2 = v2 as Vertex of G by Th10;
ex W being Walk of G st W is_Walk_from w1,w2 by GLIB_002:def 1;
hence ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 by Th19; :: thesis: verum

end;

hence G1 is connected by GLIB_002:def 1; :: thesis: verum