let G be _Graph; :: thesis: ( ex v being Vertex of G st v is isolated & G is regular implies G is edgeless )
assume A1: ( ex v being Vertex of G st v is isolated & G is regular ) ; :: thesis: G is edgeless
then consider c being Cardinal such that
A2: G is c -regular ;
c = 0 by A1, A2, Th27;
hence G is edgeless by A2; :: thesis: verum