let S be RingExtension of R; :: thesis: not S is degenerated

A1: R is Subring of S by Def1;

A1: R is Subring of S by Def1;

now :: thesis: not S is degenerated

hence
not S is degenerated
; :: thesis: verumassume
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;then 1. R = 0. S by A1, C0SP1:def 3

.= 0. R by A1, C0SP1:def 3 ;

hence contradiction ; :: thesis: verum