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