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