let PS be ParSp; :: thesis: ( ex a, b being Element of PS st
( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) implies for p, q, r, s being Element of PS holds p,q '||' r,s )
assume A1: ex a, b being Element of PS st
( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) ; :: thesis: for p, q, r, s being Element of PS holds p,q '||' r,s
let p, q, r, s be Element of PS; :: thesis: p,q '||' r,s
consider a, b being Element of PS such that
A2: ( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) by A1;
( a,b '||' a,p & a,b '||' a,q & a,b '||' a,r & a,b '||' a,s ) by A2;
then ( a,b '||' p,q & a,b '||' r,s ) by Th53;
hence p,q '||' r,s by A2, Def12; :: thesis: verum