Proof_Step_Kinds = succ (Segm 9) by NAT_1:54;
hence Proof_Step_Kinds is finite ; :: thesis: verum