:: deftheorem defines '||' PARSP_1:def 6 :
for PS being non empty ParStr
for a, b, c, d being Element of PS holds
( a,b '||' c,d iff [[a,b],[c,d]] in the CONGR of PS );