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