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

now :: thesis: not p = r

assume p = r ; :: thesis: contradiction
then A6: p,q '||' b,c by A4, Th23;
p,q '||' b,a by A2, Th23;
then b,a '||' b,c by A5, A6, Def11;
hence contradiction by A1, Th24; :: thesis: verum

end;

hence not p,q '||' p,r by A1, A2, A3, A5, Th30; :: thesis: verum