theorem Th19: :: FIELD_6:17

for S being Ring
for R being Subring of S
for x being Element of S
for x1 being Element of R st x = x1 holds
- x = - x1