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