defpred S₁[ Nat] means Polish-expression-hierarchy (T,A,T) is Polish-language;
Polish-expression-hierarchy (T,A,0) = Polish-atoms (T,A) by Def9;
then A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set U = Polish-expression-hierarchy (T,A,k);
assume S₁[k] ; :: thesis: S₁[k + 1]
then reconsider U = Polish-expression-hierarchy (T,A,k) as Polish-language of T ;
Polish-expression-hierarchy (T,A,(k + 1)) = Polish-expression-layer (T,A,U) by Th23;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence ( Polish-expression-hierarchy (T,A,n) is antichain-like & not Polish-expression-hierarchy (T,A,n) is empty ) ; :: thesis: verum