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