let SAS be Semi_Affine_Space; :: thesis: for a, b, c being Element of SAS st congr a,a,b,c holds
b = c
let a, b, c be Element of SAS; :: thesis: ( congr a,a,b,c implies b = c )
assume congr a,a,b,c ; :: thesis: b = c
then ( ( a = a & b = c ) or ex p, q being Element of SAS st
( parallelogram p,q,a,a & parallelogram p,q,b,c ) ) by Def4;
hence b = c by Th54; :: thesis: verum