take { the loopless _Graph} ; :: thesis: { the loopless _Graph} is loopless
thus { the loopless _Graph} is loopless ; :: thesis: verum