:: deftheorem defines Polish-expression-set POLNOT_1:def 11 :
for P being FinSequence-membered set
for A being Function of P,NAT holds Polish-expression-set (P,A) = union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ;