let G be _Graph; :: thesis: ( ex v being Vertex of G st v is isolated implies ( G .minDegree() = 0 & G .minInDegree() = 0 & G .minOutDegree() = 0 ) )
given v being Vertex of G such that A1: v is isolated ; :: thesis: ( G .minDegree() = 0 & G .minInDegree() = 0 & G .minOutDegree() = 0 )
A2: v .degree() = 0 by A1, GLIBPRE0:35;
for w being Vertex of G holds v .degree() c= w .degree() by A2, XBOOLE_1:2;
hence G .minDegree() = 0 by A2, Th36; :: thesis: ( G .minInDegree() = 0 & G .minOutDegree() = 0 )
A3: ( v .inDegree() = 0 & v .outDegree() = 0 ) by A1, GLIBPRE0:34;
for w being Vertex of G holds v .inDegree() c= w .inDegree() by A3, XBOOLE_1:2;
hence G .minInDegree() = 0 by A3, Th37; :: thesis: G .minOutDegree() = 0
for w being Vertex of G holds v .outDegree() c= w .outDegree() by A3, XBOOLE_1:2;
hence G .minOutDegree() = 0 by A3, Th38; :: thesis: verum