let PS be ParSp; for a, b, c, d being Element of PS st a,b '||' c,d holds
( b,a '||' c,d & a,b '||' d,c & b,a '||' d,c & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a )
let a, b, c, d be Element of PS; ( a,b '||' c,d implies ( b,a '||' c,d & a,b '||' d,c & b,a '||' d,c & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a ) )
assume
a,b '||' c,d
; ( b,a '||' c,d & a,b '||' d,c & b,a '||' d,c & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a )
then
c,d '||' a,b
by Th19;
then A1:
d,c '||' a,b
by Th21;
then A2:
d,c '||' b,a
by Th22;
then
c,d '||' b,a
by Th21;
hence
( b,a '||' c,d & a,b '||' d,c & b,a '||' d,c & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a )
by A1, A2, Th19, Th21; verum