let PS be ParSp; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum