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 A1: ( a,b congr c,x & a,b congr c,y ) ; :: thesis: x = y

A2: now

assume a = b ; :: thesis: x = y
then ( c = x & c = y ) by A1, Th55;
hence x = y ; :: thesis: verum

end;

A3: now

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

end;

now

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

end;

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