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