let c be Cardinal; :: thesis: for G being _Graph st ex v being Vertex of G st v is isolated & G is c -Dregular holds
c = 0
let G be _Graph; :: thesis: ( ex v being Vertex of G st v is isolated & G is c -Dregular implies c = 0 )
assume A1: ( ex v being Vertex of G st v is isolated & G is c -Dregular ) ; :: thesis: c = 0
then consider v being Vertex of G such that
A2: v is isolated ;
thus c = v .inDegree() by A1
.= 0 by A2, GLIB_000:156 ; :: thesis: verum