consider X being infinite disjoint_with_NAT set ;
take S = FreeUnivAlgNSG ECIW-signature ,X; :: thesis: ( S is infinite & not S is degenerated & S is well_founded & S is ECIW-strict & S is free & S is strict )
thus ( S is infinite & not S is degenerated & S is well_founded & S is ECIW-strict & S is free & S is strict ) ; :: thesis: verum