theorem Th3: :: PARSP_2:3

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:] st not a,b '||' a,c & [[a,b],[a,c]] = [[e,f],[e,g]] holds
( e <> f & e <> g & f <> g )