let G2 be _finite _Graph; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2 holds
G1 .minDegree() = min (((G2 .minDegree()) + 1),(G2 .order()))
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2 holds
G1 .minDegree() = min (((G2 .minDegree()) + 1),(G2 .order()))
let G1 be addAdjVertexAll of G2,v; :: thesis: ( not v in the_Vertices_of G2 implies G1 .minDegree() = min (((G2 .minDegree()) + 1),(G2 .order())) )
min (((G2 .minDegree()) + 1),(G2 .order())) = ((G2 .minDegree()) +` 1) /\ (G2 .order()) ;
hence ( not v in the_Vertices_of G2 implies G1 .minDegree() = min (((G2 .minDegree()) + 1),(G2 .order())) ) by Th76; :: thesis: verum