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