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 opposite a,o = opposite b,o ; :: thesis: a = b
then ( congr a,o,o, opposite a,o & congr b,o,o, opposite b,o & opposite a,o = opposite b,o ) by Th106;
then ( congr opposite a,o,o,o,a & congr opposite a,o,o,o,b ) by Th89;
hence a = b by Th81; :: thesis: verum