let PS be ParSp; :: thesis: 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; :: thesis: ( 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 ; :: thesis: p,q '||' r,s
a,b '||' p,q by A2, Th23;
hence p,q '||' r,s by A1, A3, Def11; :: thesis: verum