let SAS be Semi_Affine_Space; :: thesis: for o being Element of SAS holds opposite o,o = o
let o be Element of SAS; :: thesis: opposite o,o = o
sum o,(opposite o,o),o = o by Def6;
then sum (opposite o,o),o,o = o by Th102;
hence opposite o,o = o by Th99; :: thesis: verum