consider b being Element of SAS such that
A1: congr a,o,o,b by Th63;
take b ; :: thesis: sum (a,b,o) = o
congr o,a,b,o by A1, Th67;
hence sum (a,b,o) = o by Def5; :: thesis: verum