let G2 be locally-finite _Graph; :: thesis: 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() = (min ((v .degree()),(w .degree()))) + 1 )
let v, w be Vertex of G2; :: thesis: 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() = (min ((v .degree()),(w .degree()))) + 1 )
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = (min ((v .degree()),(w .degree()))) + 1 )
let G1 be addEdge of G2,v,e,w; :: thesis: ( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = (min ((v .degree()),(w .degree()))) + 1 )
(min ((v .degree()),(w .degree()))) + 1 = ((v .degree()) /\ (w .degree())) +` 1 ;
hence ( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = (min ((v .degree()),(w .degree()))) + 1 ) by Th70; :: thesis: verum