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