consider F being Field;
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 Th24, Th25, Th26, Th27, Th28;
then MPS F is ParSp-like by Def12;
hence ex b₁ being non empty ParStr st
( b₁ is strict & b₁ is ParSp-like ) ; :: thesis: verum