take canCompleteGraph c ; :: thesis: ( canCompleteGraph c is simple & canCompleteGraph c is c -vertex & canCompleteGraph c is complete )
thus ( canCompleteGraph c is simple & canCompleteGraph c is c -vertex & canCompleteGraph c is complete ) ; :: thesis: verum