set X = Polish-expression-layer (T,A,U);
the Element of Polish-atoms (T,A) in Polish-expression-layer (T,A,U) by Th19, TARSKI:def 3;
hence not Polish-expression-layer (T,A,U) is empty ; :: thesis: Polish-expression-layer (T,A,U) is antichain-like
let p be FinSequence; :: according to POLNOT_1:def 16 :: thesis: for q being FinSequence st p in Polish-expression-layer (T,A,U) & p ^ q in Polish-expression-layer (T,A,U) holds
q = {}
let q be FinSequence; :: thesis: ( p in Polish-expression-layer (T,A,U) & p ^ q in Polish-expression-layer (T,A,U) implies q = {} )
assume that
A11: p in Polish-expression-layer (T,A,U) and
A12: p ^ q in Polish-expression-layer (T,A,U) ; :: thesis: q = {}
consider t1 being Element of T, u1 being Element of T * such that
A13: p = t1 ^ u1 and
A14: u1 in U ^^ (A . t1) by A11, Def19;
consider t2 being Element of T, u2 being Element of T * such that
A15: p ^ q = t2 ^ u2 and
A16: u2 in U ^^ (A . t2) by A12, Def19;
t1 ^ (u1 ^ q) = t2 ^ u2 by FINSEQ_1:32, A13, A15;
then ( t1 = t2 & u1 ^ q = u2 ) by Th43;
hence q = {} by A14, A16, Def16; :: thesis: verum