let P be FinSequence-membered set ; for A being Function of P,NAT
for U, V being Subset of (P *) st U c= V holds
Polish-expression-layer (P,A,U) c= Polish-expression-layer (P,A,V)
let A be Function of P,NAT; for U, V being Subset of (P *) st U c= V holds
Polish-expression-layer (P,A,U) c= Polish-expression-layer (P,A,V)
let U, V be Subset of (P *); ( U c= V implies Polish-expression-layer (P,A,U) c= Polish-expression-layer (P,A,V) )
assume A1:
U c= V
; Polish-expression-layer (P,A,U) c= Polish-expression-layer (P,A,V)
let a be object ; TARSKI:def 3 ( not a in Polish-expression-layer (P,A,U) or a in Polish-expression-layer (P,A,V) )
assume A2:
a in Polish-expression-layer (P,A,U)
; a in Polish-expression-layer (P,A,V)
then consider p, q being FinSequence, n being Nat such that
A4:
( a = p ^ q & p in P & n = A . p & q in U ^^ n )
by Def8;
U ^^ n c= V ^^ n
by A1, TH18;
hence
a in Polish-expression-layer (P,A,V)
by A2, A4, Def8; verum