take the m + 1 -vertex Cycle-like _Graph ; :: thesis: ( the m + 1 -vertex Cycle-like _Graph is n -vertex & the m + 1 -vertex Cycle-like _Graph is n -edge & the m + 1 -vertex Cycle-like _Graph is Cycle-like )
thus ( the m + 1 -vertex Cycle-like _Graph is n -vertex & the m + 1 -vertex Cycle-like _Graph is n -edge & the m + 1 -vertex Cycle-like _Graph is Cycle-like ) ; :: thesis: verum