let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT
for U being Subset of (P *) holds Polish-atoms (P,A) c= Polish-expression-layer (P,A,U)
let A be Function of P,NAT; :: thesis: for U being Subset of (P *) holds Polish-atoms (P,A) c= Polish-expression-layer (P,A,U)
let U be Subset of (P *); :: thesis: Polish-atoms (P,A) c= Polish-expression-layer (P,A,U)
set X = Polish-atoms (P,A);
set Y = Polish-expression-layer (P,A,U);
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Polish-atoms (P,A) or a in Polish-expression-layer (P,A,U) )
assume A1: a in Polish-atoms (P,A) ; :: thesis: a in Polish-expression-layer (P,A,U)
then reconsider p = a as FinSequence ;
set q = <*> P;
A3: <*> P in U ^^ 0 by Th4;
( p in P & A . p = 0 ) by A1, Def7;
then p ^ (<*> P) in Polish-expression-layer (P,A,U) by A3, Th18;
hence a in Polish-expression-layer (P,A,U) by FINSEQ_1:34; :: thesis: verum