let T be Polish-language; :: thesis: for U being T -extending Polish-language
for V being full Polish-language of T
for W being full Polish-language of U holds
( V c= W iff W is -closed )
let U be T -extending Polish-language; :: thesis: for V being full Polish-language of T
for W being full Polish-language of U holds
( V c= W iff W is -closed )
let V be full Polish-language of T; :: thesis: for W being full Polish-language of U holds
( V c= W iff W is -closed )
let W be full Polish-language of U; :: thesis: ( V c= W iff W is -closed )
set A = Polish-arity V;
set B = Polish-arity W;
thus ( V c= W implies W is -closed ) :: thesis: ( W is -closed implies V c= W )

proof

assume V c= W ; :: thesis: W is -closed
then A2: Polish-arity V c= Polish-arity W by Th22;
W = Polish-WFF-set (U,(Polish-arity W)) ;
then A3: W is -closed ;
let p be FinSequence; :: according to POLNOT_2:def 6 :: thesis: for n being Nat
for q being FinSequence st p in T & n = (Polish-arity V) . p & q in W ^^ n holds
p ^ q in W
let n be Nat; :: thesis: for q being FinSequence st p in T & n = (Polish-arity V) . p & q in W ^^ n holds
p ^ q in W
let q be FinSequence; :: thesis: ( p in T & n = (Polish-arity V) . p & q in W ^^ n implies p ^ q in W )
assume that
A5: p in T and
A6: n = (Polish-arity V) . p and
A7: q in W ^^ n ; :: thesis: p ^ q in W
A9: T c= U by Def9;
p in dom (Polish-arity V) by A5, FUNCT_2:def 1;
then n = (Polish-arity W) . p by A2, A6, GRFUNC_1:2;
hence p ^ q in W by A3, A5, A7, A9; :: thesis: verum

end;

V = Polish-expression-set (T,(Polish-arity V)) ;
hence ( W is -closed implies V c= W ) by POLNOT_1:37; :: thesis: verum