let S be RingExtension of R; :: thesis: not S is degenerated
A1: R is Subring of S by Def1;

now :: thesis: not S is degenerated

assume S is degenerated ; :: thesis: contradiction
then 1. R = 0. S by A1, C0SP1:def 3
.= 0. R by A1, C0SP1:def 3 ;
hence contradiction ; :: thesis: verum

end;

hence not S is degenerated ; :: thesis: verum