let T be Polish-language; :: thesis: for A being Polish-arity-function of T
for F being Polish-WFF of T,A
for n being Nat st F in Polish-expression-hierarchy (T,A,(n + 1)) holds
rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n)
let A be Polish-arity-function of T; :: thesis: for F being Polish-WFF of T,A
for n being Nat st F in Polish-expression-hierarchy (T,A,(n + 1)) holds
rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n)
let F be Polish-WFF of T,A; :: thesis: for n being Nat st F in Polish-expression-hierarchy (T,A,(n + 1)) holds
rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n)
let n be Nat; :: thesis: ( F in Polish-expression-hierarchy (T,A,(n + 1)) implies rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n) )
assume F in Polish-expression-hierarchy (T,A,(n + 1)) ; :: thesis: rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n)
then reconsider G = F as Element of Polish-expression-hierarchy (T,A,(n + 1)) ;
rng (Polish-WFF-args F) = rng (Polish-WFF-args G) by Th60, Th26;
hence rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n) by FINSEQ_1:def 4; :: thesis: verum