let R be 2 -characteristic Ring; :: thesis: for a being Element of R holds - a = a
let a be Element of R; :: thesis: - a = a
Char R = 2 by RING_3:def 6;
then (0. R) * a = (2 '*' (1. R)) * a by RING_3:def 5
.= 2 '*' ((1. R) * a) by REALALG2:5
.= a + a by RING_5:2 ;
hence - a = a by RLVECT_1:6; :: thesis: verum