let PS be ParSp; for a, b, p, q, r, s being Element of PS st a <> b & p,q '||' a,b & a,b '||' r,s holds
p,q '||' r,s
let a, b, p, q, r, s be Element of PS; ( a <> b & p,q '||' a,b & a,b '||' r,s implies p,q '||' r,s )
assume that
A1:
a <> b
and
A2:
p,q '||' a,b
and
A3:
a,b '||' r,s
; p,q '||' r,s
a,b '||' p,q
by A2, Th23;
hence
p,q '||' r,s
by A1, A3, Def11; verum