let T be Polish-language; :: thesis: ( T is C -closed implies T is B -closed )
assume A1: T is C -closed ; :: thesis: T is B -closed
let p be FinSequence; :: according to POLNOT_1:def 15 :: thesis: for b₁ being set
for b₂ being set holds
( not p in dom B or not b₁ = B . p or not b₂ in T ^^ b₁ or p ^ b₂ in T )
let n be Nat; :: thesis: for b₁ being set holds
( not p in dom B or not n = B . p or not b₁ in T ^^ n or p ^ b₁ in T )
let q be FinSequence; :: thesis: ( not p in dom B or not n = B . p or not q in T ^^ n or p ^ q in T )
assume that
A4: p in dom B and
A5: n = B . p and
A6: q in T ^^ n ; :: thesis: p ^ q in T
B c= C by Def3;
then ( dom B c= dom C & n = C . p ) by A4, A5, GRFUNC_1:2;
hence p ^ q in T by A1, A4, A6; :: thesis: verum