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