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

( 0. R = 0. S & 1. R = 1. S ) by C0SP1:def 3;

hence not S is degenerated ; :: thesis: verum