let SAS be Semi_Affine_Space; :: thesis: for a, b, c, x, y being Element of SAS st congr a,b,c,x & congr a,b,c,y holds
x = y
let a, b, c, x, y be Element of SAS; :: thesis: ( congr a,b,c,x & congr a,b,c,y implies x = y )
assume A1: ( congr a,b,c,x & congr a,b,c,y ) ; :: thesis: x = y

A2: now

assume a = b ; :: thesis: x = y
then ( c = x & c = y ) by A1, Th73;
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 SAS such that
A5: parallelogram a,b,p,q by Lm1;
parallelogram p,q,a,b by A5, Th61;
then ( parallelogram p,q,c,x & parallelogram p,q,c,y ) by A1, A4, Th80;
hence x = y by Th63; :: 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, Th78;
hence x = y by Th63; :: thesis: verum

end;

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