for F being Field
for a, b, p, q, r, s being Element of (MPS F) st a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s holds
a = b