let T be Polish-language; :: thesis: for V being full Polish-language of T
for Q being Extension of V holds V c= Q
let V be full Polish-language of T; :: thesis: for Q being Extension of V holds V c= Q
let Q be Extension of V; :: thesis: V c= Q
set A = Polish-arity V;
V = Polish-expression-set (T,(Polish-arity V)) ;
hence V c= Q by POLNOT_1:37; :: thesis: verum