for F being Field
for a, b, c being Element of (MPS F)
for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:]
for K, L being Element of F st not a,b '||' a,c & [[a,b],[a,c]] = [[e,f],[e,g]] & K * ((e `1_3) - (f `1_3)) = L * ((e `1_3) - (g `1_3)) & K * ((e `2_3) - (f `2_3)) = L * ((e `2_3) - (g `2_3)) & K * ((e `3_3) - (f `3_3)) = L * ((e `3_3) - (g `3_3)) holds
( K = 0. F & L = 0. F )