set X = { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ;
set Y = union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ;
union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } c= P *

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } or a in P * )
assume a in union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ; :: thesis: a in P *
then consider Z being set such that
A1: a in Z and
A2: Z in { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } by TARSKI:def 4;
consider n being Nat such that
A3: Z = Polish-expression-hierarchy (P,A,n) by A2;
thus a in P * by A1, A3; :: thesis: verum

end;

hence union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } is Subset of (P *) ; :: thesis: verum