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