for PS being ParSp
for a, b, c being Element of PS st not a,b '||' a,c holds
( a <> b & b <> c & c <> a ) by Def11, Th18, Th20;