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