:: deftheorem Def22 defines pcs-compatible PCS_0:def 22 :
for P being pcs-Str holds
( P is pcs-compatible iff for p, p9, q, q9 being Element of P st p (--) q & p9 <= p & q9 <= q holds
p9 (--) q9 );