let G1 be _Graph; :: thesis:
let E be set ; :: thesis:
let G2 be reverseEdgeDirections of G1,E; :: thesis:
set S1 = { (v .degree()) where v is Vertex of G1 : verum } ;
set S2 = { (v .degree()) where v is Vertex of G2 : verum } ;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in { (v .degree()) where v is Vertex of G1 : verum } ; :: thesis:
then consider v1 being Vertex of G1 such that
A1: x = v1 .degree() ;
reconsider v2 = v1 as Vertex of G2 by GLIB_007:4;
x = v2 .degree() by A1, GLIBPRE0:56;
hence x in { (v .degree()) where v is Vertex of G2 : verum } ; :: thesis:

end;

assume x in { (v .degree()) where v is Vertex of G2 : verum } ; :: thesis:
then consider v2 being Vertex of G2 such that
A2: x = v2 .degree() ;
reconsider v1 = v2 as Vertex of G1 by GLIB_007:4;
x = v1 .degree() by A2, GLIBPRE0:56;
hence x in { (v .degree()) where v is Vertex of G1 : verum } ; :: thesis:

end;

hence ( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() ) by TARSKI:2; :: thesis: