let FdSp be FanodesSp; :: thesis: for a, p, b, q, c, r being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r holds
b,c '||' q,r
let a, p, b, q, c, r be Element of FdSp; :: thesis: ( 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 ; :: thesis: b,c '||' q,r
A3: ( a,p '||' c,r & a,c '||' p,r ) by A2, Def3;
not a,p,c is_collinear by A2, Def3;
then A4: not a,p '||' a,c by Def2;
not a,p,b is_collinear by A1, Def3;
then A5: not a,p '||' a,b by Def2;
( a,p '||' b,q & a,b '||' p,q ) by A1, Def3;
hence b,c '||' q,r by A5, A4, A3, Def1; :: thesis: verum