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,a,b, sum a,b,o & congr o,b,a, sum b,a,o ) by Def5;
then ( congr o,a,b, sum a,b,o & congr o,a,b, sum b,a,o ) by Th89;
hence sum a,b,o = sum b,a,o by Th81; :: thesis: verum