now :: thesis: not - (1. R) is zero

assume - (1. R) is zero ; :: thesis: contradiction
then - (- (1. R)) is zero ;
hence contradiction ; :: thesis: verum

end;

hence not - (1. R) is zero ; :: thesis: verum