take C = the (n + 1) + 1 -vertex Cycle-like _Graph; :: thesis: ( C is n + 2 -vertex & C is n + 2 -edge & C is loopless & C is Cycle-like )
C is n + 2 -vertex ;
hence ( C is n + 2 -vertex & C is n + 2 -edge & C is loopless & C is Cycle-like ) ; :: thesis: verum