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