let P be FinSequence-membered set ; :: thesis: 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; :: thesis: 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 *); :: thesis: ( U c= V implies Polish-expression-layer (P,A,U) c= Polish-expression-layer (P,A,V) )
assume A1: U c= V ; :: thesis: Polish-expression-layer (P,A,U) c= Polish-expression-layer (P,A,V)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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 Def6;
U ^^ n c= V ^^ n by A1, Th17;
hence a in Polish-expression-layer (P,A,V) by A2, A4, Def6; :: thesis: verum