set F = the Field;
for a, b, c, d, p, q, r, s being Element of (MPS the Field) 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 the Field) st
( a,b '||' c,x & a,c '||' b,x ) ) by Th13, Th14, Th15, Th16, Th17;
then MPS the Field is ParSp-like ;
hence ex b₁ being non empty ParStr st
( b₁ is strict & b₁ is ParSp-like ) ; :: thesis: verum