set S = Polynom-Ring L;
( 0. (Polynom-Ring L) = 0_. L & 1. (Polynom-Ring L) = 1_. L ) by POLYNOM3:def 10;
hence not Polynom-Ring L is degenerated ; :: thesis: verum