consider b being Element of SAS such that
A1: congr a,o,o,b by Th82;
take b ; :: thesis: sum a,b,o = o
congr o,a,b,o by A1, Th87;
hence sum a,b,o = o by Def5; :: thesis: verum