let PS be ParSp; 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; ( 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
; 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; verum