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