let G be _Graph; :: thesis: ( G .minDegree() = 0 implies ex v being Vertex of G st v is isolated )
assume G .minDegree() = 0 ; :: thesis: ex v being Vertex of G st v is isolated
then consider v being Vertex of G such that
A1: v .degree() = 0 and
for w being Vertex of G holds v .degree() c= w .degree() by Th36;
take v ; :: thesis: v is isolated
thus v is isolated by A1, GLIBPRE0:35; :: thesis: verum