let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is with_max_degree iff G2 is with_max_degree )
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E holds
( G1 is with_max_degree iff G2 is with_max_degree )
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( G1 is with_max_degree iff G2 is with_max_degree )
consider F being PGraphMapping of G1,G2 such that
A1: ( F = id G1 & F is isomorphism ) by GLIBPRE0:77;
thus ( G1 is with_max_degree iff G2 is with_max_degree ) by A1, Th83; :: thesis: verum