let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E holds
( G1 .order() = G2 .order() & G1 .size() = G2 .size() )
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E holds
( G1 .order() = G2 .order() & G1 .size() = G2 .size() )
let G1 be reverseEdgeDirections of G2,E; :: thesis: ( G1 .order() = G2 .order() & G1 .size() = G2 .size() )
A1: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by Th4;
thus G1 .order() = card (the_Vertices_of G1) by GLIB_000:def 24
.= G2 .order() by A1, GLIB_000:def 24 ; :: thesis: G1 .size() = G2 .size()
thus G1 .size() = card (the_Edges_of G1) by GLIB_000:def 25
.= G2 .size() by A1, GLIB_000:def 25 ; :: thesis: verum