for P being pcs-Str
for D being non empty Subset-Family of P
for p, q being Element of (pcs-general-power D) st ( for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 ) ) holds
p <= q