let FdSp be FanodesSp; for a, b, c, p, q, r being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r holds
b,c '||' q,r
let a, b, c, p, q, r be Element of FdSp; ( parallelogram a,p,b,q & parallelogram a,p,c,r implies b,c '||' q,r )
assume that
A1:
parallelogram a,p,b,q
and
A2:
parallelogram a,p,c,r
; b,c '||' q,r
A3:
( a,p '||' c,r & a,c '||' p,r )
by A2;
not a,p,c are_collinear
by A2;
then A4:
not a,p '||' a,c
;
not a,p,b are_collinear
by A1;
then A5:
not a,p '||' a,b
;
( a,p '||' b,q & a,b '||' p,q )
by A1;
hence
b,c '||' q,r
by A5, A4, A3, Def1; verum