let SAS be Semi_Affine_Space; :: thesis: for a, b, o being Element of SAS holds
( diff a,b,o = o iff a = b )
let a, b, o be Element of SAS; :: thesis: ( diff a,b,o = o iff a = b )
( diff a,b,o = o implies a = b )

proof

assume diff a,b,o = o ; :: thesis: a = b
then opposite a,o = opposite b,o by Def6;
hence a = b by Th107; :: thesis: verum

end;

hence ( diff a,b,o = o iff a = b ) by Def6; :: thesis: verum