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 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
then consider a, b being Element of PS such that
A1: a <> b and
A2: for c being Element of PS holds a,b '||' a,c ;
let p, q, r, s be Element of PS; :: thesis: p,q '||' r,s
( a,b '||' a,r & a,b '||' a,s ) by A2;
then A3: a,b '||' r,s by Th35;
( a,b '||' a,p & a,b '||' a,q ) by A2;
then a,b '||' p,q by Th35;
hence p,q '||' r,s by A1, A3, Def11; :: thesis: verum