let P be FinSequence-membered set ; 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; 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 ; ( Q is A -closed implies Polish-expression-set (P,A) c= Q )
assume A1:
Q is A -closed
; Polish-expression-set (P,A) c= Q
let a be object ; TARSKI:def 3 ( not a in Polish-expression-set (P,A) or a in Q )
assume
a in Polish-expression-set (P,A)
; a in Q
then consider n being Nat such that
A2:
a in Polish-expression-hierarchy (P,A,(n + 1))
by Th37;
thus
a in Q
by A1, A2, Th53, TARSKI:def 3; verum