let PS be ParSp; :: thesis: for a, b being Element of PS holds a,b '||' a,b
let a, b be Element of PS; :: thesis: a,b '||' a,b
b,a '||' b,b by Def11;
hence a,b '||' a,b by Def11; :: thesis: verum