let FdSp be FanodesSp; :: thesis: 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; :: 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;
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; :: thesis: verum