set S1 = S;
let S2 be Language-like ; :: thesis: ( S2 is S -extending implies not S2 is degenerated )
assume S2 is S -extending ; :: thesis: not S2 is degenerated
then ( TheEqSymbOf S = TheEqSymbOf S2 & TheNorSymbOf S = TheNorSymbOf S2 ) ;
then ( 0. S = 0. S2 & 1. S = 1. S2 ) ;
hence not S2 is degenerated ; :: thesis: verum