let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT
for a being object st a in Polish-expression-set (P,A) holds
ex n being Nat st a in Polish-expression-hierarchy (P,A,(n + 1))
let A be Function of P,NAT; :: thesis: for a being object st a in Polish-expression-set (P,A) holds
ex n being Nat st a in Polish-expression-hierarchy (P,A,(n + 1))
let a be object ; :: thesis: ( a in Polish-expression-set (P,A) implies ex n being Nat st a in Polish-expression-hierarchy (P,A,(n + 1)) )
assume A1: a in Polish-expression-set (P,A) ; :: thesis: ex n being Nat st a in Polish-expression-hierarchy (P,A,(n + 1))
set Y = { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ;
consider X being set such that
A2: a in X and
A3: X in { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } by A1, TARSKI:def 4;
consider n being Nat such that
A4: X = Polish-expression-hierarchy (P,A,n) by A3;
Polish-expression-hierarchy (P,A,n) c= Polish-expression-hierarchy (P,A,(n + 1)) by Th24;
hence ex n being Nat st a in Polish-expression-hierarchy (P,A,(n + 1)) by A2, A4; :: thesis: verum