set U = Polish-atoms (T,A);
consider a being object such that
A4: ( a in T & A . a = 0 ) by Def18;
( not Polish-atoms (T,A) is empty & Polish-atoms (T,A) c= T ) by A4, Def7;
hence ( not Polish-atoms (T,A) is empty & Polish-atoms (T,A) is antichain-like ) ; :: thesis: verum