let C be _Graph; :: thesis: ( C is n + 2 -vertex & C is Cycle-like implies C is simple )
assume ( C is n + 2 -vertex & C is Cycle-like ) ; :: thesis: C is simple
then ( C is m + 3 -vertex & C is Cycle-like ) ;
hence C is simple ; :: thesis: verum