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 Th82; :: thesis: verum
end;
hence ( diff (a,b,o) = o iff a = b ) by Def6; :: thesis: verum