let PS be ParSp; :: thesis: for a, b, c, p, q, r, s being Element of PS st not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & a,c '||' p,s & b,c '||' q,r & b,c '||' q,s holds
r = s
let a, b, c, p, q, r, s be Element of PS; :: thesis: ( not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & a,c '||' p,s & b,c '||' q,r & b,c '||' q,s implies r = s )
assume that
A1: not a,b '||' a,c and
A2: a,b '||' p,q and
A3: a,c '||' p,r and
A4: a,c '||' p,s and
A5: b,c '||' q,r and
A6: b,c '||' q,s ; :: thesis: r = s

A7: now :: thesis: ( p <> q implies r = s )

b <> c by A1, Th18;
then A8: q,r '||' q,s by A5, A6, Def11;
a <> c by A1, Def11;
then A9: p,r '||' p,s by A3, A4, Def11;
assume p <> q ; :: thesis: r = s
then not p,q '||' p,r by A1, A2, A3, A5, Th31;
hence r = s by A9, A8, Th33; :: thesis: verum

end;

( p = q implies ( p = r & p = s ) ) by A1, A3, A4, A5, A6, Th32;
hence r = s by A7; :: thesis: verum