let SAS be Semi_Affine_Space; :: thesis: for a, o, b being Element of SAS st opposite a,o = opposite b,o holds
a = b
let a, o, b be Element of SAS; :: thesis: ( opposite a,o = opposite b,o implies a = b )
assume A1: opposite a,o = opposite b,o ; :: thesis: a = b
congr a,o,o, opposite a,o by Th106;
then A2: congr opposite a,o,o,o,a by Th89;
congr b,o,o, opposite b,o by Th106;
then congr opposite a,o,o,o,b by A1, Th89;
hence a = b by A2, Th81; :: thesis: verum