let SAS be Semi_Affine_Space; :: thesis: for a, b, o being Element of SAS holds sum a,b,o = sum b,a,o
let a, b, o be Element of SAS; :: thesis: sum a,b,o = sum b,a,o
congr o,b,a, sum b,a,o by Def5;
then congr o,a,b, sum b,a,o by Th89;
hence sum a,b,o = sum b,a,o by Def5; :: thesis: verum