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

now :: thesis: for x being object holds
( ( x in { (v .degree()) where v is Vertex of G1 : verum } implies x in { (v .degree()) where v is Vertex of G2 : verum } ) & ( x in { (v .degree()) where v is Vertex of G2 : verum } implies x in { (v .degree()) where v is Vertex of G1 : verum } ) )

let x be object ; :: thesis: ( ( x in { (v .degree()) where v is Vertex of G1 : verum } implies x in { (v .degree()) where v is Vertex of G2 : verum } ) & ( x in { (v .degree()) where v is Vertex of G2 : verum } implies x in { (v .degree()) where v is Vertex of G1 : verum } ) )

hereby :: thesis: ( x in { (v .degree()) where v is Vertex of G2 : verum } implies x in { (v .degree()) where v is Vertex of G1 : verum } )

assume x in { (v .degree()) where v is Vertex of G1 : verum } ; :: thesis: x in { (v .degree()) where v is Vertex of G2 : verum }
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:54;
hence x in { (v .degree()) where v is Vertex of G2 : verum } ; :: thesis: verum

end;

assume x in { (v .degree()) where v is Vertex of G2 : verum } ; :: thesis: x in { (v .degree()) where v is Vertex of G1 : verum }
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:54;
hence x in { (v .degree()) where v is Vertex of G1 : verum } ; :: thesis: verum

end;

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