let n be Element of NAT ; :: thesis: - (0.REAL n) = 0.REAL n
(0.REAL n) + (0.REAL n) = 0.REAL n by EUCLID:31;
hence - (0.REAL n) = 0.REAL n by EUCLID:41; :: thesis: verum