:: deftheorem defines props LTLAXIO1:def 10 :
for b₁ being Subset of LTLB_WFF holds
( b₁ = props iff for x being set holds
( x in b₁ iff ex n being Element of NAT st x = prop n ) );