theorem Th70: :: GLIB_013:70

for G2 being _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1 )