theorem Th16: :: PARSP_1:16

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