let FdSp be FanodesSp; :: thesis: for a, b, c, x, y being Element of FdSp st a,b congr c,x & a,b congr c,y holds
x = y
let a, b, c, x, y be Element of FdSp; :: thesis: ( a,b congr c,x & a,b congr c,y implies x = y )
assume that
A1: a,b congr c,x and
A2: a,b congr c,y ; :: thesis: x = y

A3: now

assume that
a <> b and
A4: not a,b,c is_collinear ; :: thesis: x = y
( parallelogram a,b,c,x & parallelogram a,b,c,y ) by A1, A2, A4, Th60;
hence x = y by Th43; :: thesis: verum

end;

A5: now

assume that
A6: a <> b and
A7: a,b,c is_collinear ; :: thesis: x = y
consider p, q being Element of FdSp such that
A8: parallelogram a,b,p,q by A6, Th51;
parallelogram p,q,a,b by A8, Th41;
then ( parallelogram p,q,c,x & parallelogram p,q,c,y ) by A1, A2, A7, Th62;
hence x = y by Th43; :: thesis: verum

end;

now

assume A9: a = b ; :: thesis: x = y
then c = x by A1, Th55;
hence x = y by A2, A9, Th55; :: thesis: verum

end;

hence x = y by A5, A3; :: thesis: verum