let G be _Graph; :: thesis: ( G is n -vertex & G is Cycle-like implies G is n -edge )
assume A1: ( G is n -vertex & G is Cycle-like ) ; :: thesis: G is n -edge
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 ;
C .size() = (P .size()) + 1 by GLIB_000:52
.= P .order() by GLIB_002:46
.= C .order() by GLIB_000:def 33
.= n by A1, GLIB_013:def 3 ;
hence G is n -edge by GLIB_013:def 4; :: thesis: verum