let PS be ParSp; :: thesis: for a, b, c, d being Element of PS st a,b '||' a,c & a,b '||' a,d holds
a,b '||' c,d
let a, b, c, d be Element of PS; :: thesis: ( a,b '||' a,c & a,b '||' a,d implies a,b '||' c,d )
assume that
A1: a,b '||' a,c and
A2: a,b '||' a,d ; :: thesis: a,b '||' c,d

now :: thesis: ( a <> b & a <> c implies a,b '||' c,d )

assume that
A3: a <> b and
A4: a <> c ; :: thesis: a,b '||' c,d
a,c '||' a,d by A1, A2, A3, Def11;
then a,c '||' c,d by Th24;
hence a,b '||' c,d by A1, A4, Th26; :: thesis: verum

end;

hence a,b '||' c,d by A2, Th20; :: thesis: verum