let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E holds
( G1 .componentSet() = G2 .componentSet() & G1 .numComponents() = G2 .numComponents() )
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E holds
( G1 .componentSet() = G2 .componentSet() & G1 .numComponents() = G2 .numComponents() )
let G1 be reverseEdgeDirections of G2,E; :: thesis: ( G1 .componentSet() = G2 .componentSet() & G1 .numComponents() = G2 .numComponents() )
for V being object holds
( V in G1 .componentSet() iff V in G2 .componentSet() )

proof

let V be object ; :: thesis: ( V in G1 .componentSet() iff V in G2 .componentSet() )

hereby :: thesis: ( V in G2 .componentSet() implies V in G1 .componentSet() )

assume V in G1 .componentSet() ; :: thesis: V in G2 .componentSet()
then consider v being Vertex of G1 such that
A1: V = G1 .reachableFrom v by GLIB_002:def 8;
reconsider w = v as Vertex of G2 by Th10;
V = G2 .reachableFrom w by A1, Th20;
hence V in G2 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

assume V in G2 .componentSet() ; :: thesis: V in G1 .componentSet()
then consider v being Vertex of G2 such that
A2: V = G2 .reachableFrom v by GLIB_002:def 8;
reconsider w = v as Vertex of G1 by Th10;
V = G1 .reachableFrom w by A2, Th20;
hence V in G1 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

hence A3: G1 .componentSet() = G2 .componentSet() by TARSKI:2; :: thesis: G1 .numComponents() = G2 .numComponents()
thus G1 .numComponents() = card (G2 .componentSet()) by A3, GLIB_002:def 9
.= G2 .numComponents() by GLIB_002:def 9 ; :: thesis: verum