:: deftheorem Def11 defines ParSp-like PARSP_1:def 12 :
for IT being non empty ParStr holds
( IT is ParSp-like iff for a, b, c, d, p, q, r, s being Element of IT holds
( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of IT st
( a,b '||' c,x & a,c '||' b,x ) ) );