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;
then A3: ( b,c '||' c,b & b,a '||' c,p ) by PARSP_1:23, PARSP_1:25;
a,b '||' c,q by A2;
then A4: b,a '||' c,q by PARSP_1:23;
a,c '||' b,p by A1;
then A5: c,a '||' b,p by PARSP_1:23;
a,c '||' b,q by A2;
then A6: c,a '||' b,q by PARSP_1:23;
not b,c,a are_collinear by A1, Th28;
then not b,c '||' b,a ;
hence p = q by A3, A4, A5, A6, PARSP_1:34; :: thesis: verum