:: deftheorem defprops defines props PL_AXIOM:def 7 :
for b₁ being Subset of PL-WFF holds
( b₁ = props iff for x being set holds
( x in b₁ iff ex n being Element of NAT st x = Prop n ) );