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

proof

set U = Polish-expression-hierarchy (P,A,0);
set V = Polish-expression-hierarchy (P,A,1);
A3: Polish-expression-hierarchy (P,A,1) = Polish-expression-hierarchy (P,A,(0 + 1))
.= Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,0))) by Th23 ;
Polish-expression-hierarchy (P,A,0) = Polish-atoms (P,A) by Def9;
hence S₁[ 0 ] by A3, Th19; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: S₁[k] ; :: thesis: S₁[k + 1]
set U = Polish-expression-hierarchy (P,A,k);
set V = Polish-expression-hierarchy (P,A,(k + 1));
A13: Polish-expression-hierarchy (P,A,(k + 1)) = Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,k))) by Th23;
Polish-expression-hierarchy (P,A,((k + 1) + 1)) = Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,(k + 1)))) by Th23;
hence S₁[k + 1] by A11, A13, Th20; :: thesis: verum

end;

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