:: deftheorem defines Prop PL_AXIOM:def 6 :
for n being Element of NAT holds Prop n = <*(3 + n)*>;