theorem Th17: :: CQC_THE1:21

0 in Proof_Step_Kinds & ... & 9 in Proof_Step_Kinds ;