let C be _Graph; :: thesis: ( C is n + 2 -vertex & C is Cycle-like implies C is loopless )
assume A1: ( C is n + 2 -vertex & C is Cycle-like ) ; :: thesis: C is loopless
assume not C is loopless ; :: thesis: contradiction
then consider v, e being object such that
A2: e Joins v,v,C by GLIB_000:18;
C .walkOf (v,e,v) is Cycle-like by A2, GLIB_001:156;
then the_Vertices_of C = (C .walkOf (v,e,v)) .vertices() by A1, Th39
.= {v,v} by A2, GLIB_001:91
.= {v} by ENUMSET1:29 ;
then A3: C .order() = 1 by CARD_1:30;
A4: C .order() = n + 2 by A1, GLIB_013:def 3;
n + 2 >= 0 + 2 by XREAL_1:6;
hence contradiction by A3, A4; :: thesis: verum