:: deftheorem Def35 defines pcs-chain-like PCS_0:def 35 :
for C being Relation holds
( C is pcs-chain-like iff for P, Q being pcs-Str st P in rng C & Q in rng C & not P c= Q holds
Q c= P );