let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT holds Polish-atoms (P,A) c= Polish-expression-set (P,A)
let A be Function of P,NAT; :: thesis: Polish-atoms (P,A) c= Polish-expression-set (P,A)
Polish-expression-set (P,A) is A -closed by TH51;
hence Polish-atoms (P,A) c= Polish-expression-set (P,A) by Th52; :: thesis: verum