let PS be ParSp; :: thesis: ( ( for a, b being Element of PS holds a = b ) implies for p, q, r, s being Element of PS holds p,q '||' r,s )
assume A1: for a, b being Element of PS holds a = b ; :: thesis: for p, q, r, s being Element of PS holds p,q '||' r,s
let p, q, r, s be Element of PS; :: thesis: p,q '||' r,s
r = s by A1;
hence p,q '||' r,s by Def11; :: thesis: verum