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