let SAS be Semi_Affine_Space; :: thesis: for a, b, o being Element of SAS st opposite (a,o) = opposite (b,o) holds
a = b
let a, b, o 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 Th81;
then A2: congr opposite (a,o),o,o,a by Th69;
congr b,o,o, opposite (b,o) by Th81;
then congr opposite (a,o),o,o,b by A1, Th69;
hence a = b by A2, Th62; :: thesis: verum