theorem :: PCS_0:22

for P being pcs-Str
for a being set
for p, q being Element of (pcs-extension (P,a)) st p = a holds
p <= q