take R --> (0. S) ; :: thesis: R --> (0. S) is additive
thus R --> (0. S) is additive ; :: thesis: verum