let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() )
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() )
let G2 be reverseEdgeDirections of G1,E; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() ) )
assume A1: v1 = v2 ; :: thesis: ( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() )

per cases ( E c= the_Edges_of G1 or not E c= the_Edges_of G1 ) ;

suppose E c= the_Edges_of G1 ; :: thesis: ( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() )

then A2: ( v2 .edgesIn() = ((v1 .edgesIn()) \ E) \/ ((v1 .edgesOut()) /\ E) & v2 .edgesOut() = ((v1 .edgesOut()) \ E) \/ ((v1 .edgesIn()) /\ E) ) by A1, Th58;
thus v2 .edgesInOut() = ((((v1 .edgesIn()) \ E) \/ ((v1 .edgesOut()) /\ E)) \/ ((v1 .edgesIn()) /\ E)) \/ ((v1 .edgesOut()) \ E) by A2, XBOOLE_1:4
.= ((((v1 .edgesIn()) \ E) \/ ((v1 .edgesIn()) /\ E)) \/ ((v1 .edgesOut()) /\ E)) \/ ((v1 .edgesOut()) \ E) by XBOOLE_1:4
.= ((v1 .edgesIn()) \/ ((v1 .edgesOut()) /\ E)) \/ ((v1 .edgesOut()) \ E) by XBOOLE_1:51
.= (v1 .edgesIn()) \/ (((v1 .edgesOut()) /\ E) \/ ((v1 .edgesOut()) \ E)) by XBOOLE_1:4
.= v1 .edgesInOut() by XBOOLE_1:51 ; :: thesis: v2 .degree() = v1 .degree()
thus v2 .degree() = ((card ((v1 .edgesIn()) \ E)) +` (card ((v1 .edgesOut()) /\ E))) +` (card (((v1 .edgesOut()) \ E) \/ ((v1 .edgesIn()) /\ E))) by A2, Th2, CARD_2:35
.= ((card ((v1 .edgesIn()) \ E)) +` (card ((v1 .edgesOut()) /\ E))) +` ((card ((v1 .edgesOut()) \ E)) +` (card ((v1 .edgesIn()) /\ E))) by Th2, CARD_2:35
.= (((card ((v1 .edgesIn()) \ E)) +` (card ((v1 .edgesOut()) /\ E))) +` (card ((v1 .edgesIn()) /\ E))) +` (card ((v1 .edgesOut()) \ E)) by CARD_2:19
.= (((card ((v1 .edgesIn()) \ E)) +` (card ((v1 .edgesIn()) /\ E))) +` (card ((v1 .edgesOut()) /\ E))) +` (card ((v1 .edgesOut()) \ E)) by CARD_2:19
.= ((card (((v1 .edgesIn()) \ E) \/ ((v1 .edgesIn()) /\ E))) +` (card ((v1 .edgesOut()) /\ E))) +` (card ((v1 .edgesOut()) \ E)) by Th2, CARD_2:35
.= ((v1 .inDegree()) +` (card ((v1 .edgesOut()) /\ E))) +` (card ((v1 .edgesOut()) \ E)) by XBOOLE_1:51
.= (v1 .inDegree()) +` ((card ((v1 .edgesOut()) /\ E)) +` (card ((v1 .edgesOut()) \ E))) by CARD_2:19
.= (v1 .inDegree()) +` (card (((v1 .edgesOut()) /\ E) \/ ((v1 .edgesOut()) \ E))) by Th2, CARD_2:35
.= v1 .degree() by XBOOLE_1:51 ; :: thesis: verum

end;

suppose not E c= the_Edges_of G1 ; :: thesis: ( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() )

then G1 == G2 by GLIB_007:def 1;
hence ( v2 .edgesInOut() = v1 .edgesInOut() & v2 .degree() = v1 .degree() ) by A1, GLIB_000:96; :: thesis: verum

end;

end;