let G be _Graph; :: thesis: ( G is n -edge & G is Cycle-like implies G is n -vertex )
assume A2: ( G is n -edge & G is Cycle-like ) ; :: thesis: G is n -vertex
then reconsider C = G as Cycle-like _Graph ;
set e = the Edge of C;
reconsider P = the removeEdge of C, the Edge of C as _finite Path-like _Graph ;
G .order() = P .order() by GLIB_000:def 33
.= (P .size()) + 1 by GLIB_002:46
.= C .size() by GLIB_000:52
.= n by A2, GLIB_013:def 4 ;
hence G is n -vertex by GLIB_013:def 3; :: thesis: verum