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-set (P,A)
let A be Function of P,NAT; :: thesis: for n being Nat holds Polish-expression-hierarchy (P,A,n) c= Polish-expression-set (P,A)
let n be Nat; :: thesis: Polish-expression-hierarchy (P,A,n) c= Polish-expression-set (P,A)
set Q = Polish-expression-hierarchy (P,A,n);
set X = { (Polish-expression-hierarchy (P,A,m)) where m is Nat : verum } ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Polish-expression-hierarchy (P,A,n) or a in Polish-expression-set (P,A) )
assume A1: a in Polish-expression-hierarchy (P,A,n) ; :: thesis: a in Polish-expression-set (P,A)
Polish-expression-hierarchy (P,A,n) in { (Polish-expression-hierarchy (P,A,m)) where m is Nat : verum } ;
hence a in Polish-expression-set (P,A) by A1, TARSKI:def 4; :: thesis: verum