set T = pcs-total D;
pcs-total D is trivial ;
then for x, y being Element of (pcs-total D) st x <= y & y <= x holds
x = y by STRUCT_0:def 10;
hence pcs-total D is antisymmetric by YELLOW_0:def 3; :: thesis: verum