:: deftheorem Def6 defines Polish-expression-layer POLNOT_1:def 19 :
for T being Polish-language
for A being Polish-arity-function of T
for U being Polish-language of T
for b₄ being Subset of (T *) holds
( b₄ = Polish-expression-layer (T,A,U) iff for a being object holds
( a in b₄ iff ex t being Element of T ex u being Element of T * st
( a = t ^ u & u in U ^^ (A . t) ) ) );