theorem Th17: :: PARSP_1:17

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