let PS be ParSp; 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; ( not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r implies p = r )
assume that
A1:
( not a,b '||' a,c & a,c '||' p,r )
and
A2:
b,c '||' p,r
; p = r
A3:
p,r '||' b,c
by A2, Th23;
( not a,c '||' b,c & p,r '||' a,c )
by A1, Th23, Th29;
hence
p = r
by A3, Def11; verum