let F be Field; :: thesis: MPS F is ParSp
for a, b, c, d, p, q, r, s being Element of (MPS F) holds
( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of (MPS F) st
( a,b '||' c,x & a,c '||' b,x ) ) by PARSP_1:13, PARSP_1:14, PARSP_1:15, PARSP_1:16, PARSP_1:17;
hence MPS F is ParSp by PARSP_1:def 12; :: thesis: verum