:: deftheorem defines pcs-like PCS_0:def 23 :
for P being pcs-Str holds
( P is pcs-like iff ( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible ) );