A1: 9 in { k where k is Element of NAT : k <= 9 } ;
thus not Proof_Step_Kinds is empty by A1; :: thesis: verum