set Y = Polish-expression-set (T,A);
Polish-expression-hierarchy (T,A,0) c= Polish-expression-set (T,A) by Th26;
then reconsider Y = Polish-expression-set (T,A) as non empty Subset of (T *) ;
Y is antichain-like

proof

let p be FinSequence; :: according to POLNOT_1:def 16 :: thesis: for q being FinSequence st p in Y & p ^ q in Y holds
q = {}
let q be FinSequence; :: thesis: ( p in Y & p ^ q in Y implies q = {} )
assume that
A2: p in Y and
A3: p ^ q in Y ; :: thesis: q = {}
consider m being Nat such that
A10: p in Polish-expression-hierarchy (T,A,(m + 1)) by A2, Th28;
consider n being Nat such that
A11: p ^ q in Polish-expression-hierarchy (T,A,(n + 1)) by A3, Th28;
set B = Polish-expression-hierarchy (T,A,((m + 1) + (n + 1)));
A12: Polish-expression-hierarchy (T,A,(m + 1)) c= Polish-expression-hierarchy (T,A,((m + 1) + (n + 1))) by Th25;
A13: Polish-expression-hierarchy (T,A,(n + 1)) c= Polish-expression-hierarchy (T,A,((m + 1) + (n + 1))) by Th25;
Polish-expression-hierarchy (T,A,((m + 1) + (n + 1))) is antichain-like ;
hence q = {} by A10, A11, A12, A13; :: thesis: verum

end;

hence Polish-expression-set (T,A) is Polish-language of T ; :: thesis: verum