theorem Th17: :: CQC_THE1:21
0 in Proof_Step_Kinds & ... & 9 in Proof_Step_Kinds ;