take canDCompleteGraph c ; :: thesis: ( canDCompleteGraph c is Dsimple & canDCompleteGraph c is c -vertex & canDCompleteGraph c is Dcomplete )
thus ( canDCompleteGraph c is Dsimple & canDCompleteGraph c is c -vertex & canDCompleteGraph c is Dcomplete ) ; :: thesis: verum