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 ( parallelogram a,b,c,p & parallelogram a,b,c,q ) ; :: thesis: p = q
then ( not b,c,a is_collinear & a,b '||' c,p & a,c '||' b,p & a,b '||' c,q & a,c '||' b,q ) by Def3, Th36;
then ( not b,c '||' b,a & b,c '||' c,b & b,a '||' c,p & b,a '||' c,q & c,a '||' b,p & c,a '||' b,q ) by Def2, PARSP_1:40, PARSP_1:42;
hence p = q by PARSP_1:52; :: thesis: verum