let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT
for Q being FinSequence-membered set
for n being Nat st Q is A -closed holds
Polish-expression-hierarchy (P,A,n) c= Q
let A be Function of P,NAT; :: thesis: for Q being FinSequence-membered set
for n being Nat st Q is A -closed holds
Polish-expression-hierarchy (P,A,n) c= Q
let Q be FinSequence-membered set ; :: thesis: for n being Nat st Q is A -closed holds
Polish-expression-hierarchy (P,A,n) c= Q
let n be Nat; :: thesis: ( Q is A -closed implies Polish-expression-hierarchy (P,A,n) c= Q )
assume A1: Q is A -closed ; :: thesis: Polish-expression-hierarchy (P,A,n) c= Q
defpred S₁[ Nat] means Polish-expression-hierarchy (P,A,$1) c= Q;
A2: S₁[ 0 ]

proof

Polish-expression-hierarchy (P,A,0) = Polish-atoms (P,A) by Def9;
hence S₁[ 0 ] by A1, Th34; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set V = Polish-expression-hierarchy (P,A,k);
assume A4: Polish-expression-hierarchy (P,A,k) c= Q ; :: thesis: S₁[k + 1]
for a being object st a in Polish-expression-hierarchy (P,A,(k + 1)) holds
a in Q

proof

let a be object ; :: thesis: ( a in Polish-expression-hierarchy (P,A,(k + 1)) implies a in Q )
assume a in Polish-expression-hierarchy (P,A,(k + 1)) ; :: thesis: a in Q
then a in Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,k))) by Th23;
then consider p, q being FinSequence, n being Nat such that
A5: a = p ^ q and
A6: p in P and
A7: n = A . p and
A8: q in (Polish-expression-hierarchy (P,A,k)) ^^ n by Def6;
A9: dom A = P by FUNCT_2:def 1;
q in Q ^^ n by A4, A8, Th17, TARSKI:def 3;
hence a in Q by A1, A5, A6, A7, A9; :: thesis: verum

end;

hence S₁[k + 1] by TARSKI:def 3; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence Polish-expression-hierarchy (P,A,n) c= Q ; :: thesis: verum