f - f = f + (- f) by VALUED_1:def 9
.= (1 (#) f) + ((- 1) (#) f) by VALUED_1:def 6
.= (1 + (- 1)) (#) f by TOPREALC:2
.= 0 (#) f ;
hence f - f is empty-yielding ; :: thesis: verum