let R be commutative p -characteristic Ring; :: thesis: not R is degenerated
( Char R = p & p > 1 ) by RING_3:def 6, INT_2:def 4;
hence not R is degenerated by REALALG2:23; :: thesis: verum