theorem :: PARSP_1:7

for F being Field
for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff [[a,b],[c,d]] in PR F ) ;