set P = the n + 1 -vertex Path-like _Graph;

per cases ( n = 0 or n > 0 ) ;

suppose A1: n = 0 ; :: thesis: ex b₁ being _Graph st
( b₁ is n + 1 -vertex & b₁ is n + 1 -edge & b₁ is Cycle-like )

set v = the Vertex of the n + 1 -vertex Path-like _Graph;
take C = the addEdge of the n + 1 -vertex Path-like _Graph, the Vertex of the n + 1 -vertex Path-like _Graph, {} , the Vertex of the n + 1 -vertex Path-like _Graph; :: thesis: ( C is n + 1 -vertex & C is n + 1 -edge & C is Cycle-like )
C is Cycle-like by A1, Th41;
hence ( C is n + 1 -vertex & C is n + 1 -edge & C is Cycle-like ) ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex b₁ being _Graph st
( b₁ is n + 1 -vertex & b₁ is n + 1 -edge & b₁ is Cycle-like )

then n + 1 > 0 + 1 by XREAL_1:6;
then the n + 1 -vertex Path-like _Graph .order() > 0 + 1 by GLIB_013:def 3;
then A3: not the n + 1 -vertex Path-like _Graph is _trivial by GLIB_000:26;
consider P0 being vertex-distinct Path of the n + 1 -vertex Path-like _Graph such that
( P0 .vertices() = the_Vertices_of the n + 1 -vertex Path-like _Graph & P0 .edges() = the_Edges_of the n + 1 -vertex Path-like _Graph ) and
A4: ( Endvertices the n + 1 -vertex Path-like _Graph = {(P0 .first()),(P0 .last())} iff not the n + 1 -vertex Path-like _Graph is _trivial ) and
( P0 is trivial iff the n + 1 -vertex Path-like _Graph is _trivial ) and
A5: ( P0 is closed iff the n + 1 -vertex Path-like _Graph is _trivial ) and
P0 is minlength by Th31;
reconsider v1 = P0 .first() , v2 = P0 .last() as Element of Endvertices the n + 1 -vertex Path-like _Graph by A3, A4, TARSKI:def 2;
A6: P0 .first() <> P0 .last() by A3, A5, GLIB_001:def 24;
take C = the addEdge of the n + 1 -vertex Path-like _Graph,v1, the_Edges_of the n + 1 -vertex Path-like _Graph,v2; :: thesis: ( C is n + 1 -vertex & C is n + 1 -edge & C is Cycle-like )
not the_Edges_of the n + 1 -vertex Path-like _Graph in the_Edges_of the n + 1 -vertex Path-like _Graph ;
then C is Cycle-like by A3, A6, Th42;
hence ( C is n + 1 -vertex & C is n + 1 -edge & C is Cycle-like ) ; :: thesis: verum

end;

end;