theorem :: PARSP_1:37

for PS being ParSp st ex a, b being Element of PS st
( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) holds
for p, q, r, s being Element of PS holds p,q '||' r,s