let G be _Graph; :: thesis: ( G is Cycle-like implies ( not G is edgeless & G is _finite & G is with_max_degree ) )
assume A1: G is Cycle-like ; :: thesis: ( not G is edgeless & G is _finite & G is with_max_degree )
hence not G is edgeless ; :: thesis: ( G is _finite & G is with_max_degree )
reconsider G9 = G as Cycle-like _Graph by A1;
set C = the Cycle-like Walk of G9;
( the Cycle-like Walk of G9 .vertices() = the_Vertices_of G & the Cycle-like Walk of G9 .edges() = the_Edges_of G ) by Th39;
hence ( G is _finite & G is with_max_degree ) by GLIB_000:def 17; :: thesis: verum