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