let PS be ParSp; :: thesis: for a, b, c, p, r being Element of PS st not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r holds
p = r
let a, b, c, p, r be Element of PS; :: thesis: ( not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r implies p = r )
assume ( not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r ) ; :: thesis: p = r
then ( not a,c '||' b,c & p,r '||' a,c & p,r '||' b,c ) by Th40, Th47;
hence p = r by Def12; :: thesis: verum