set V = Polish-expression-set (F₁(),F₂());
consider U being set such that
A2: for a being object holds
( a in U iff ( a in Polish-expression-set (F₁(),F₂()) & P₁[a] ) ) from XBOOLE_0:sch 1();
A3: U c= Polish-expression-set (F₁(),F₂()) by A2;
then reconsider U = U as Subset of (F₁() *) by XBOOLE_1:1;
U is F₂() -closed

proof

let p be FinSequence; :: according to POLNOT_1:def 15 :: thesis: for n being Nat
for q being FinSequence st p in F₁() & n = F₂() . p & q in U ^^ n holds
p ^ q in U
let n be Nat; :: thesis: for q being FinSequence st p in F₁() & n = F₂() . p & q in U ^^ n holds
p ^ q in U
let q be FinSequence; :: thesis: ( p in F₁() & n = F₂() . p & q in U ^^ n implies p ^ q in U )
assume that
A4: p in F₁() and
A5: n = F₂() . p and
A6: q in U ^^ n ; :: thesis: p ^ q in U
A7: U ^^ n c= (Polish-expression-set (F₁(),F₂())) ^^ n by A3, TH18;
then A8: P₁[p ^ q] by A1, A4, A5, A6;
Polish-expression-set (F₁(),F₂()) is F₂() -closed by TH51;
hence p ^ q in U by A2, A4, A5, A6, A7, A8; :: thesis: verum

end;

then Polish-expression-set (F₁(),F₂()) c= U by Th55;
hence for a being object st a in Polish-expression-set (F₁(),F₂()) holds
P₁[a] by A2; :: thesis: verum