theorem Th13: :: PARSP_1:13

for F being Field
for a, b being Element of (MPS F) holds a,b '||' b,a