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-atoms (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-atoms (P,A) c= Q
let Q be FinSequence-membered set ; :: thesis: ( Q is A -closed implies Polish-atoms (P,A) c= Q )
assume A0: Q is A -closed ; :: thesis: Polish-atoms (P,A) c= Q
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Polish-atoms (P,A) or a in Q )
assume A1: a in Polish-atoms (P,A) ; :: thesis: a in Q
then reconsider a = a as FinSequence ;
dom A = P by FUNCT_2:def 1;
then A3: ( a in dom A & A . a = 0 ) by A1, Def7;
{} in Q ^^ 0 by Th4;
then a ^ {} in Q by A0, A3;
hence a in Q by FINSEQ_1:34; :: thesis: verum