let PS be ParSp; :: thesis: for p, q, r, s being Element of PS st not p,q '||' p,r & p,r '||' p,s & q,r '||' q,s holds
r = s
let p, q, r, s be Element of PS; :: thesis: ( not p,q '||' p,r & p,r '||' p,s & q,r '||' q,s implies r = s )
assume that
A1: ( not p,q '||' p,r & p,r '||' p,s ) and
A2: q,r '||' q,s ; :: thesis: r = s
A3: r,s '||' r,q by A2, Th29;
( not r,p '||' r,q & r,s '||' r,p ) by A1, Th29;
hence r = s by A3, Def11; :: thesis: verum