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