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