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 by STRUCT_0:def 8; :: thesis: verum