theorem :: PARSP_1:34

for PS being ParSp
for a, b, c, p, q, r, s being Element of PS st not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & a,c '||' p,s & b,c '||' q,r & b,c '||' q,s holds
r = s