let FdSp be FanodesSp; :: thesis: for a, b, c, p, q being Element of FdSp st parallelogram a,b,c,p & parallelogram a,b,c,q holds
p = q
let a, b, c, p, q be Element of FdSp; :: thesis: ( parallelogram a,b,c,p & parallelogram a,b,c,q implies p = q )
assume that
A1: parallelogram a,b,c,p and
A2: parallelogram a,b,c,q ; :: thesis: p = q
a,b '||' c,p by A1, Def3;
then A3: ( b,c '||' c,b & b,a '||' c,p ) by PARSP_1:23, PARSP_1:25;
a,b '||' c,q by A2, Def3;
then A4: b,a '||' c,q by PARSP_1:23;
a,c '||' b,p by A1, Def3;
then A5: c,a '||' b,p by PARSP_1:23;
a,c '||' b,q by A2, Def3;
then A6: c,a '||' b,q by PARSP_1:23;
not b,c,a is_collinear by A1, Th36;
then not b,c '||' b,a by Def2;
hence p = q by A3, A4, A5, A6, PARSP_1:34; :: thesis: verum