let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT
for Q being FinSequence-membered set st Q is A -closed holds
Polish-expression-set (P,A) c= Q
let A be Function of P,NAT; :: thesis: for Q being FinSequence-membered set st Q is A -closed holds
Polish-expression-set (P,A) c= Q
let Q be FinSequence-membered set ; :: thesis: ( Q is A -closed implies Polish-expression-set (P,A) c= Q )
assume A1: Q is A -closed ; :: thesis: Polish-expression-set (P,A) c= Q
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Polish-expression-set (P,A) or a in Q )
assume a in Polish-expression-set (P,A) ; :: thesis: a in Q
then consider n being Nat such that
A2: a in Polish-expression-hierarchy (P,A,(n + 1)) by Th28;
thus a in Q by A1, A2, Th35, TARSKI:def 3; :: thesis: verum