let S be Subring of R; :: thesis: not S is degenerated
( 0. R = 0. S & 1. R = 1. S ) by C0SP1:def 3;
hence not S is degenerated ; :: thesis: verum