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