for PS being ParSp
for a, b, c, d being Element of PS st ( a = b or c = d or ( a = c & b = d ) or ( a = d & b = c ) ) holds
a,b '||' c,d by Def11, Th18, Th20;